proposition: Lemma uniq_path_ucycle_extend_1 m n m' l (mn : g m n) (nm' : g n m') (Hl : path (except g n) m' (rcons l m)) (Hun : uniq (rcons (m' :: l) m)) : ucycle g [:: m, n, m' & l].
proof: Proof. apply/andP; split. by rewrite /= mn nm' /=; move/except_path : Hl. apply uniq_extend_1 => //; try by rewrite (simple_neg simple_g). by move: Hl; rewrite rcons_path => /andP[/path_except_notin]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext