proposition: Lemma subcycle_trans : transitive subcycle.
proof: Proof. move=> r p q sub_p_r /subcycleP [m sub_r_q]. move: sub_p_r; rewrite -(subcycle_rot_r m) => /subcycleP [n] sub_p_r. by apply/subcycleP; exists n; apply: subseq_trans sub_r_q. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)