proposition: Lemma root_notin_subgraph (Hg : simple g) n m : m \in successors n -> n \notin subgraph m n.
proof: Proof. rewrite 2!inE => gnm; rewrite negb_and -implybE gnm implyTb. apply/connectP => -[[_ /=| h s]]. - apply/eqP/negP => /eqP nm; move: gnm; rewrite nm; by apply/negP. - move=> /path_except_notin => /negP ns nsm; apply ns. by rewrite nsm /= mem_last. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext