proposition: Lemma trivIset_sub_ver_suc_suc_helper (Hg : simple g) m n1 n2 m2 l : g m n1 -> g m n2 -> g n2 m2 -> m2 != m -> path (except g n2) m2 l -> uniq (m2 :: l) -> n1 = last m2 l -> False.
proof: Proof. move=> mn1 mn2 n2m2 m2m Hl Hun Hlast. suff : ucycle g [:: m, n2, m2 & l] by apply acyclic_g. apply/andP; split. by rewrite /= mn2 /= n2m2 /= rcons_path -Hlast (except_path Hl) symmetric_g. rewrite -(cat1s m) -(cat1s n2) catA cat_uniq Hun andbT. apply/andP; split; first by rewrite /= andbT inE (simple_neg Hg). rewrite /= negb_or !inE negb_or -andbA andbCA eq_sym (simple_neg Hg) // m2m /=. apply/hasP; case => x Hx /=. rewrite 2!inE. case/orP => /eqP ?; subst x; last first. move/path_except_notin : Hl; by rewrite Hx. case/splitPr : Hx => l1 l2 in Hl Hun Hlast. suff : ucycle g [:: m, n2, m2 & l1] by apply acyclic_g. apply/andP; split. rewrite /= mn2 n2m2 /=. by move: Hl; rewrite -cat_rcons cat_path => /andP[/except_path]. rewrite [m2 :: _]lock /= -lock. move: (Hun) => Hun'. move: Hun; rewrite -{1}(cat1s m2) catA cat_uniq => /and3P[-> _ _]. rewrite andbT /= !inE /= !negb_or /= (simple_neg Hg) //=. rewrite eq_sym m2m /= (simple_neg Hg) //=; apply/andP; split; last first. by move/path_except_notin : Hl; rewrite mem_cat negb_or => /andP[]. move: Hun'; rewrite -(cat1s m2) uniq_catC -(cat1s m) cat_uniq => /andP[]. by rewrite catA cat_uniq => /andP[]; rewrite uniq_catC /= => /andP[]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext