proposition: Lemma Vgraph_not0 m0 n0 : 0 < #|'V(m0, n0)|.
proof: Proof. rewrite card_gt0. apply/set0Pn => /=. eexists; exact: root_in_Vgraph. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition