proposition: Lemma successor_subgraph_successor (Hg : simple g) n0 m0 m1 : g n0 m0 -> m1 != m0 -> m1 \in subgraph g m0 n0 -> ~~ g m1 n0.
proof: Proof. move=> n0m0 m1m0. rewrite inE => /andP[_ /connectP[p]]. case/shortenP => p' Hp' Hun p'p Hlast. apply/negP => abs. suff : ucycle g [:: n0, m0 & p']. apply acyclic_g => /=. move: Hlast. destruct p' => //= /eqP; by rewrite (negbTE m1m0). apply/andP; split. by rewrite /= n0m0 /= rcons_path -Hlast abs andbT (except_path Hp'). rewrite -(cat1s n0) cat_uniq Hun andbT /= negb_or inE /=. rewrite eq_sym (simple_neg Hg n0m0) /=. move/path_except_notin : Hp'; apply: contra. rewrite -has_pred1 (@eq_in_has _ _ (pred1 n0)) // => x /=; by rewrite inE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext