proposition: Lemma mem_subcycle p s : subcycle p s -> {subset p <= s}.
proof: Proof. move=> /subcycleP[n /mem_subseq sub_p_s] z z_p. by apply: sub_p_s; rewrite mem_rot. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(preliminaries)