proposition: Lemma mono_cycle_in s : {in P &, {mono f : x y / e x y >-> e' x y}} -> all P s -> cycle e' (map f s) = cycle e s.
proof: Proof. by move=> f_mono; rewrite cycle_map; apply: eq_in_cycle. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)