proposition: Lemma notin_Vgraph_part_vnode (n0 : 'I_n) : n0 \notin cover (Vgraph_part_vnode n0).
proof: Proof. apply/bigcupP => /=; case=> E /imsetP [] /= m0 Hm0 ->; by rewrite 2!inE eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2