proposition: Lemma uniq_path_ucycle_extend_3 m n m' l n1 m'1 (mn : g m n) (nm' : g n m') (mn1 : g m n1) (n1m'1 : g n1 m'1) (n1n : n1 != n) (m'm : m' != m) (m'1m : m'1 != m) (Hl : path (except g n) m' (rcons l m'1)) (Hun : uniq (m' :: l)) : ucycle g [:: m'1, n1, m, n, m' & l].
proof: Proof. apply/andP; split. rewrite /path.cycle -cats1 -(cat1s n1) -(cat1s m) -(cat1s n) -(cat1s m') !catA. rewrite -(catA _ l) cat_path /= andbT mn nm' symmetric_g n1m'1 symmetric_g mn1. by rewrite /= cats1 (except_path Hl). rewrite -(cat1s m) -(cat1s n) catA -(cat1s n1) catA -(cat1s m'1) catA cat_uniq Hun andbT. have n1m : n1 != m by rewrite (simple_neg simple_g) // symmetric_g. have m'1n : m'1 != n by move: Hl; rewrite rcons_path /= eq_sym => /andP[_] /except13. have m_not_n : m != n by rewrite (simple_neg simple_g). have m'1n1 : m'1 != n1 by rewrite (simple_neg simple_g) // symmetric_g. apply/andP; split. by rewrite /= !inE !negb_or andbT m'1n /= andbT n1m /= m'1n1 /= m_not_n andbT m'1m. apply/hasP; case => x. rewrite inE => /orP[/eqP ->{x} /=|xl]. apply/negP. rewrite !inE !negb_or m'm /= (@eq_sym _ m' n) (simple_neg simple_g nm') andbT. apply/andP; split; (apply/eqP => ?; subst m'). - suff : ucycle g [:: m'1; n1; m; n] by apply acyclic_g. rewrite /ucycle /= !inE !negb_or andbT symmetric_g n1m'1 /= symmetric_g. by rewrite mn1 /= mn /= andbT nm' /= m'1n1 /= m'm m'1n /= n1m /= n1n. - suff : ucycle g [:: m ; n ; n1] by apply acyclic_g. apply/andP; split; first by rewrite /= mn /= nm' /= andbT symmetric_g. by rewrite /= andbT mem_seq1 eq_sym n1n andbT mem_seq2 negb_or m_not_n /= eq_sym. rewrite /= !inE => /orP[/eqP xm'1|]. move: xl; rewrite {}xm'1 {x} => m'1l. case/splitPr : m'1l => l1 l2 in Hl Hun. suff : ucycle g (m'1 :: n1 :: m :: n :: m' :: l1) by apply acyclic_g. apply uniq_path_ucycle_extend_2 => //; [by rewrite symmetric_g|by rewrite eq_sym| |]. 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 m_not_n. rewrite mem_rcons inE eq_sym negb_or m'1m /=; apply/negP => ml1. case/splitPr : ml1 => l11 l12 in Hl Hun. suff : ucycle g [:: m, n, m' & l11] by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //. by move: Hl; rewrite -cat_rcons rcons_cat cat_path => /andP[Hl]. move: Hun. rewrite -2!cat_cons -(cat1s m) catA -(catA _ _ (m'1 :: _)) cat_uniq => /and3P[Hun _ _]. by rewrite -cats1. move: Hun; rewrite -cat_cons cat_uniq => /and3P[Hun _ _]. rewrite cons_uniq Hun andbT inE negb_or (simple_neg simple_g) //=. by move/path_except_notin : Hl; rewrite rcons_cat mem_cat negb_or => /andP[]. case/orP => [/eqP xn1|]. move: xl; rewrite {}xn1 => n1l. case/splitPr : n1l => l1 l2 in Hl Hun. suff : ucycle g [:: n1, m, n, m' & l1] by apply acyclic_g. apply: uniq_path_ucycle_extend_2 => //. by move: Hl; rewrite rcons_path -cat_rcons cat_path -andbA => /andP[]. by move: Hun; rewrite -cat_cons cat_uniq => /andP[]. case/orP => [/eqP xm|/eqP xn]. move: xl; rewrite {}xm {x} => ml. case/splitPr : ml => l1 l2 in Hl Hun. suff : ucycle g [:: m, n, m' & l1] 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 => /and3P[]. move: xl; rewrite {}xn {x} => nl. 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