[STATEMENT]
lemma non_empty_cycle_root_move_root_forward:
  assumes "non_empty_cycle_root r x"
      and "point q"
      and "r \<le> x\<^sup>\<star>;q"
    shows "non_empty_cycle_root q x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. non_empty_cycle_root q x
[PROOF STEP]
by (metis assms backward_finite_path_root_move_root non_empty_cycle_root_no_start_end_points
          non_empty_cycle_root_point_exchange non_empty_cycle_root_rtc_start_points)