proposition: Lemma mono_cycle : {mono f : x y / e x y >-> e' x y} -> {mono map f : s / cycle e s >-> cycle e' s}.
proof: Proof. by move=> ? ?; rewrite cycle_map; apply: eq_cycle. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)