proposition: Lemma notin_subgraph (Hg : simple g) n1 m0 n0 m1 : g n0 m0 -> g n1 m0 -> n1 != n0 -> g n1 m1 -> m1 != m0 -> n0 \notin subgraph g m1 n1.
proof: Proof. move=> n0m0 n1m0 n1n0 n1m1 m1m0. rewrite inE negb_and n1m1 /=. apply/negP => abs. case/connectP : abs => p. case/shortenP => p' Hp' Hun p'p Hlast. suff : ucycle g [:: m0, n1, m1 & p'] by apply acyclic_g. apply/andP; split. rewrite [m1 :: _]lock /= -lock rcons_path symmetric_g n1m0 /= n1m1 /=. by rewrite (@except_path _ _ n1) // -Hlast. rewrite -(cat1s m0) -(cat1s n1) catA cat_uniq Hun andbT. apply/andP; split. by rewrite /= inE andbT eq_sym (simple_neg Hg n1m0). apply/hasP; case=> x. rewrite inE. case/orP => [/eqP ->{x} | Hx]. by rewrite /= inE (negbTE m1m0) /= inE eq_sym (negbTE (simple_neg Hg n1m1)). rewrite /= inE. case/orP. move/eqP => ?; subst x. case/splitPr : Hx => p1 p2 in Hp' Hun p'p Hlast. suff : ucycle g [:: m0, n1, m1 & p1] by apply acyclic_g. apply uniq_path_ucycle_extend_1 => //. by rewrite symmetric_g. by move: Hp'; rewrite -(cat1s m0) catA cat_path -cats1 => /andP[]. by move: Hun; rewrite -cat_cons -(cat1s m0) catA cat_uniq cats1 => /andP[]. rewrite inE => /eqP xm1. move/path_except_notin : Hp'; by rewrite -{}xm1 Hx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext