proposition: Lemma subcycle_rot_r n p s : subcycle p (rot n s) = subcycle p s.
proof: Proof. apply/subcycleP/subcycleP => -[m sub]. have [k _ sub'] := subseq_rot (size (rot n s) - n) sub. rewrite -/(rotr _ _) rotK rot_rot_add in sub'; eexists; exact sub'. have [k _ sub'] := subseq_rot n sub. by exists (rot_add p m k); rewrite -rot_rot_add. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)