[STATEMENT]
lemma non_empty_cycle_root_move_root_loop:
  assumes "non_empty_cycle_root r x"
      and "point q"
      and "q \<le> x\<^sup>\<star>;r"
    shows "q \<le> x\<^sup>+;q"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. q \<le> x\<^sup>+ ; q
[PROOF STEP]
using assms non_empty_cycle_root_loop_converse non_empty_cycle_root_move_root
[PROOF STATE]
proof (prove)
using this:
non_empty_cycle_root r x
point q
q \<le> x\<^sup>\<star> ; r
non_empty_cycle_root ?r ?x \<Longrightarrow> ?r \<le> ?x\<^sup>+ ; ?r
\<lbrakk>non_empty_cycle_root ?r ?x; point ?q; ?q \<le> ?x\<^sup>\<star> ; ?r\<rbrakk> \<Longrightarrow> non_empty_cycle_root ?q ?x

goal (1 subgoal):
 1. q \<le> x\<^sup>+ ; q
[PROOF STEP]
by blast