proposition: Lemma uniq_path_ucycle_cat x m n2 l2 l1 n1 (n2m : g n2 m) (n1m : g n1 m) (n2n1 : n2 != n1) (Hl1 : path (except g m) n1 (rcons l1 x)) (Hl2 : path (except g m) n2 (rcons l2 x)) (Hun1 : uniq (n1 :: l1)) (Hun2 : uniq (n2 :: l2)) : ucycle g ((x :: rev l2) ++ [:: n2, m, n1 & l1]).
proof: Proof. move: Hl1 Hl2 Hun1 Hun2. move Hp : (size (l1 ++ l2)) => p. move: l1 l2 Hp x n2 m n2m n1 n1m n2n1. elim: p {-2}p (leqnn p). case=> // _ [] // [] // _ x /=. move=> n2 m n2m n1 n1m n2n1. rewrite !andbT exceptE /=. case/and3P => H1 H2 H3. case/and3P => L2 K2 K3 _ _. apply/andP; split. by rewrite /= symmetric_g L2 /= symmetric_g symmetric_g /= H1 n2m symmetric_g n1m. rewrite /= !inE !negb_or /= andbT. rewrite (simple_neg simple_g) /=; last by rewrite symmetric_g. rewrite K3 /=. rewrite (simple_neg simple_g) /=; last by rewrite symmetric_g. by rewrite K2 /= n2n1 /= eq_sym. move=> p IH p' Hp' l1 l2 Hp x. move=> n2 m n2m n1 n1m n2n1. move=> Hl1 Hl2 Hun1 Hun2. apply/andP; split. rewrite /= rcons_cat /= -(cat1s n2) catA cat_path. apply/andP; split. move/except_path: Hl2. rewrite -rev_path (_ : rev (belast _ _) = rev l2 ++ [:: n2]); last first. by rewrite (_ : [:: n2] = rev [:: n2]) // -rev_cat lastI belast_rcons /=. rewrite cats1 last_rcons. apply: sub_path => a b; by rewrite symmetric_g. by rewrite last_cat /= n2m /= symmetric_g n1m /= (except_path Hl1). rewrite -(cat1s x) -catA uniq_catC. rewrite -catA. rewrite -(cat1s n2). rewrite catA. rewrite catA. rewrite -(catA _ _ [:: x]). rewrite cat_uniq. apply/andP; split; first by rewrite cats1 -rev_cons rev_uniq. apply/andP; split. apply/hasP; case => y. rewrite mem_cat. case/orP. rewrite inE. case/orP. move/eqP => ?; subst y. rewrite /= mem_cat. case/orP. rewrite mem_rev => n2l2. move/path_except_notin : Hl2. by rewrite mem_rcons inE n2l2 orbC. rewrite inE. apply/negP; by rewrite (simple_neg simple_g) // symmetric_g. rewrite inE. case/orP => [|yl1]. move/eqP => ?; subst y. rewrite /= mem_cat mem_rev mem_seq1 eq_sym (negbTE n2n1) orbF => Hm. case/splitPr : Hm => l21 l22 in Hl2 Hun2. suff : ucycle g [:: n1, m, n2 & l21] by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //; first by rewrite symmetric_g. by move: Hl2; rewrite -cat_rcons rcons_cat cat_path => /andP[]. by move: Hun2; rewrite -cat_cons -(cat1s n1) catA cat_uniq cats1 => /and3P[]. rewrite ?inE mem_cat mem_seq1 => /orP[|]. rewrite mem_rev => yl2. case/splitPr : yl1 => l11 l12 in Hl1 Hun1 Hp. case/splitPr : yl2 => l21 l22 in Hl2 Hun2 Hp. suff : ucycle g ((y :: rev l21) ++ n2 :: m :: n1 :: l11). apply acyclic_g; by rewrite /= size_cat /= 2!addnS. apply (IH (size (l11 ++ l21))) => //. apply (@leq_trans p'.-1). rewrite -Hp !size_cat /= 3!addnS /= addSnnS -!addnA leq_add2l. by rewrite -addnS addnC -addnA leq_addr. rewrite -(leq_add2r 1) 2!addn1. apply: leq_trans Hp'. rewrite -ltnS prednK //; first by rewrite -Hp 2!size_cat /= addnS addSn. by move: Hl1; rewrite rcons_path -cat_rcons cat_path -andbA => /and3P[]. by move: Hl2; rewrite -(cat1s y) catA rcons_cat cats1 cat_path => /andP[]. by move: Hun1; rewrite -cat_cons cat_uniq => /and3P[]. by move: Hun2; rewrite -cat_cons cat_uniq => /and3P[]. move/eqP => ?; subst y. case/splitPr : yl1 => l11 l12 in Hl1 Hun1. suff : ucycle g [:: n2, m, n1 & l11] by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //; first by rewrite symmetric_g. by move: Hl1; rewrite -cat_rcons rcons_path cat_path -andbA => /andP[]. by move: Hun1; rewrite -cat_cons -(cat1s n2) catA cat_uniq cats1 => /and3P[]. rewrite inE => /eqP ?; subst y. rewrite /= mem_cat mem_seq1 => /orP[|]. rewrite mem_rev. move=> xl2. case/splitPr : xl2 => l21 l22 in Hl2 Hun2 Hp. suff : ucycle g ((x :: rev l1) ++ n1 :: m :: n2 :: l21). apply acyclic_g; by rewrite /= size_cat /= 2!addnS. apply (IH (size (l1 ++ l21))) => //. apply (@leq_trans p'.-1). by rewrite -Hp !size_cat /= 2!addnS /= leq_add2l leq_addr. by rewrite -subn1 leq_subLR -addn1. by rewrite 2!size_cat addnC. by rewrite eq_sym. by move: Hl2; rewrite -cat_rcons rcons_cat cat_path => /andP[]. by move: Hun2; rewrite -cat_cons cat_uniq => /andP[]. move/eqP => ?; subst x. suff : ucycle g [:: n2, m, n1 & l1] by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //; first by rewrite symmetric_g. rewrite rcons_uniq Hun1 andbT inE negb_or n2n1 /=. apply/negP => n2l1. case/splitPr : n2l1 => l11 l12 in Hl1 Hun1 Hp. suff : ucycle g (n2 :: m :: n1 :: l11) by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //; first by rewrite symmetric_g. by move: Hl1; rewrite -cat_rcons rcons_cat cat_path => /andP[]. by move: Hun1; rewrite -cat_cons -(cat1s n2) catA cat_uniq cats1 => /and3P[]. rewrite -(cat1s m) -(cat1s n1). rewrite uniq_catC. rewrite (catA [:: x]). rewrite cat_uniq Hun1 andbT. apply/andP; split. rewrite /= andbT inE. apply/eqP => ?; subst x. move/path_except_notin : Hl1. by rewrite -cats1 mem_cat inE eqxx orbT. apply/hasP; case => y. rewrite inE. case/orP => [ | yl1]. move/eqP => ?; subst y. rewrite /= inE. case/orP. move/eqP => ?; subst x. suff : ucycle g [:: n1, m, n2 & l2] by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //. by rewrite symmetric_g. rewrite rcons_uniq Hun2 andbT inE negb_or eq_sym n2n1 /=. apply/negP => n1l2. case/splitPr : n1l2 => l21 l22 in Hl2 Hun2. suff : ucycle g [:: n1, m, n2 & l21] by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //; first by rewrite symmetric_g. by move: Hl2; rewrite -cat_rcons rcons_cat cat_path => /andP[]. by move: Hun2; rewrite -cat_cons -(cat1s n1) catA cat_uniq cats1 => /and3P[]. rewrite inE. apply/negP; by rewrite (simple_neg simple_g). rewrite ?inE /= ?in_cons ?inE . case/orP. move/eqP => ?; subst y. case/splitPr : yl1 => l11 l12 in Hl1 Hun1 Hp. suff : ucycle g ((x :: rev l2) ++ n2 :: m :: n1 :: l11). apply acyclic_g; by rewrite /= size_cat /= 2!addnS. apply (IH (size (l11 ++ l2))) => //. apply (@leq_trans p'.-1). by rewrite -Hp !size_cat addnS addSn /= -addnA leq_add2l leq_addl. by rewrite -subn1 leq_subLR -addn1. by move: Hl1; rewrite -cat_rcons; rewrite rcons_cat cat_path => /andP[]. by move: Hun1; rewrite -cat_cons cat_uniq => /and3P[]. move/eqP => ?; subst y. move/path_except_notin : Hl1. by rewrite mem_rcons inE yl1 orbC. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext