proposition: Lemma uniq_path_ucycle_extend_2 m n m' l n1 (nm : g m n) (nm' : g n m') (mn1 : g m n1) (m'm : m' != m) (Hl : path (except g n) m' (rcons l n1)) (Hun : uniq (m' :: l)) : ucycle g [:: n1, m, n, m' & l].
proof: Proof. apply/andP; split. rewrite /= symmetric_g mn1 nm nm' /=; exact: except_path Hl. rewrite -(cat1s m) -(cat1s n) catA -(cat1s n1) catA cat_uniq Hun andbT. have n1m : n1 != m by rewrite (simple_neg simple_g) // symmetric_g. have n1n : n1 != n by move: Hl; rewrite eq_sym rcons_path => /andP[_ /except13]. have mn : m != n by rewrite (simple_neg simple_g). apply/andP; split; first by rewrite /= !inE negb_or andbT n1m /= n1n. apply/hasP; case => x. rewrite in_cons => /orP[/eqP ->{x}|xl]. rewrite /= !inE (negbTE m'm) /=. apply/negP; rewrite negb_or andbC eq_sym (simple_neg simple_g) //=. apply/eqP => m'n1. suff : ucycle g [:: m; n; n1] by apply acyclic_g. rewrite /ucycle /= andbT nm /= andbT -m'n1 nm' /= m'n1 symmetric_g mn1 /=. by rewrite mem_seq1 eq_sym n1n andbT mem_seq2 negb_or mn eq_sym. rewrite /= !inE => /orP[/eqP xn1|]. move: xl; rewrite {}xn1 {x} => xl. case/splitPr : xl => k11 k12 in Hl Hun. suff : ucycle g [:: n1, m, n, m' & k11] by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //; first by rewrite symmetric_g. move: Hl; rewrite -cat_rcons rcons_cat cat_path => /andP[Hl _] /=. rewrite (sub_path_except _ _ Hl) // ?andbT 1?eq_sym //. by rewrite exceptE /= nm' eq_sym mn. rewrite mem_rcons inE negb_or eq_sym n1m /=; apply/negP => mk11. case/splitPr : mk11 => k111 k112 in Hl Hun. suff : ucycle g [:: m, n, m' & k111] by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //. by move: Hl; rewrite -cat_rcons rcons_cat cat_path => /andP[]. move: Hun; rewrite -2!cat_cons -(cat1s m) catA -(catA _ _ (n1 :: k12)). by rewrite cat_uniq cats1 => /and3P[]. move: Hun; rewrite -(cat1s n1) -(cat1s m') 2!catA cat_uniq cats1 => /andP[Hun _]. rewrite rcons_cons cons_uniq mem_rcons inE negb_or eq_sym n1n andTb Hun andbT. move/path_except_notin : Hl; rewrite rcons_cat mem_cat negb_or => /andP[nk11 _]. by rewrite inE negb_or nk11 andbT (simple_neg simple_g). case/orP => [/eqP xm|/eqP xn]. move: xl; rewrite {}xm {x} => ml. case/splitPr : ml => k11 k12 in Hl Hun. suff : ucycle g [:: m, n, m' & k11] by apply acyclic_g. apply: uniq_path_ucycle_extend_1 => //. by move: Hl; rewrite -cat_rcons rcons_cat cat_path => /andP[]. by move: Hun; rewrite -cat_cons -(cat1s m) catA cat_uniq cats1 => /andP[]. move: xl; rewrite {}xn {x}. by move: Hl; rewrite rcons_path => /andP[/path_except_notin] /negP. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext