[STATEMENT]
lemma omega_mult_star_2:
  "x\<^sup>\<omega> * y\<^sup>\<star> = x\<^sup>\<omega>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. x\<^sup>\<omega> * y\<^sup>\<star> = x\<^sup>\<omega>
[PROOF STEP]
by (meson order.antisym le_supE star.circ_back_loop_prefixpoint omega_sub_vector)