proposition: Lemma uniq_path_ucycle_cat_extend x m n2 m2 l2 l1 n1 m1 (mn2 : g m n2) (n2m2 : g n2 m2) (mn1 : g m n1) (n1m1 : g n1 m1) (n1n2 : n1 != n2) (m2m : m2 != m) (m1m : m1 != m) (Hl1 : path (except g n1) m1 (rcons l1 x)) (Hl2 : path (except g n2) m2 (rcons l2 x)) (Hunl1 : uniq (m1 :: l1)) (Hunl2 : uniq (m2 :: l2)) : ucycle g ((x :: rev l2) ++ [:: m2, n2, m, n1, m1 & l1]).
proof: Proof. rewrite -(cat1s m2) catA. rewrite cat_cons. rewrite (_ : rev l2 ++ [:: m2] = rev (m2 :: l2)); last first. by rewrite rev_cons cats1. apply uniq_path_ucycle_cat => //. by rewrite symmetric_g. by rewrite symmetric_g. by rewrite eq_sym. rewrite /=. apply/andP; split. by rewrite exceptE /= n1m1 m1m andbT /= eq_sym (simple_neg simple_g). apply: sub_path_except (Hl1) => //; first by rewrite eq_sym. rewrite mem_rcons inE orbC; apply/negP. case/orP. move=> yl1. case/splitPr : yl1 => l11 l12 in Hl1 Hunl1. suff : ucycle g (m :: n1 :: m1 :: l11) by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //. by move: Hl1; rewrite -cat_rcons rcons_cat cat_path => /andP[]. by move: Hunl1; rewrite -cat_cons -(cat1s m) catA cats1 cat_uniq => /and3P[]. move/eqP => ?; subst x. suff : ucycle g (m :: n1 :: m1 :: l1) by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //. rewrite rcons_uniq Hunl1 andbT inE negb_or eq_sym m1m /=. apply/negP => ml1. case/splitPr : ml1 => l11 l12 in Hl1 Hunl1. suff : ucycle g (m :: n1 :: m1 :: l11) by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //. by move: Hl1; rewrite -cat_rcons rcons_cat cat_path => /andP[]. by move: Hunl1; rewrite -cat_cons -(cat1s m) catA cat_uniq cats1 => /and3P[]. rewrite -(cat1s m2) rcons_cat cat_path /= andbT. apply/andP; split. rewrite exceptE /= n2m2 /= (simple_neg simple_g) //=; by rewrite symmetric_g. apply: sub_path_except (Hl2) => //; first by rewrite eq_sym. rewrite mem_rcons inE orbC ; apply/negP => /orP[|]. move=> yl2. case/splitPr : yl2 => l21 l22 in Hl2 Hunl2. suff : ucycle g (m :: n2 :: m2 :: l21) by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //. by move: Hl2; rewrite -cat_rcons rcons_cat cat_path => /andP[]. by move: Hunl2; rewrite -cat_cons -(cat1s m) catA cats1 cat_uniq => /and3P[]. move/eqP => ?; subst x. suff : ucycle g (m :: n2 :: m2 :: l2) by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //. rewrite rcons_uniq Hunl2 andbT inE negb_or eq_sym m2m /=. apply/negP => ml2. case/splitPr : ml2 => l21 l22 in Hl2 Hunl2. suff : ucycle g (m :: n2 :: m2 :: l21) by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //. by move: Hl2; rewrite -cat_rcons rcons_cat cat_path => /andP[]. by move: Hunl2; rewrite -cat_cons -(cat1s m) catA cats1 cat_uniq => /and3P[]. rewrite -(cat1s n1) cat_uniq Hunl1 /= andbT !inE /= negb_or. rewrite (simple_neg simple_g) //=; last by rewrite symmetric_g. apply/hasP; case => y yl1 /=. rewrite inE. move/eqP => ?; subst y. by move/path_except_notin : Hl1; rewrite mem_rcons inE yl1 orbC. rewrite -(cat1s n2) cat_uniq Hunl2 /= andbT !inE /= negb_or. rewrite (simple_neg simple_g) //=; last by rewrite symmetric_g. apply/hasP; case => y yl2 /=. rewrite inE. move/eqP => ?; subst y. by move/path_except_notin : Hl2; rewrite mem_rcons inE yl2 orbC. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext