proposition: Lemma cycle_morph l : path.cycle g l = path.cycle g' (map f l).
proof: Proof. case:l => //= *; by rewrite -map_rcons (@map_path _ _ _ _ g pred0) // has_pred0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist