proposition: Lemma subcycle_uniq p s : subcycle p s -> uniq s -> uniq p.
proof: Proof. move=> /subcycleP [n sub_p_s]; rewrite -(rot_uniq n p). exact: subseq_uniq. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)