proposition: Lemma homo_cycle : {homo f : x y / e x y >-> e' x y} -> {homo map f : s / cycle e s >-> cycle e' s}.
proof: Proof. by move=> f_homo s hs; rewrite cycle_map (sub_cycle _ hs). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)