proposition: Lemma disjoint_Vgraph (m0 m1 : 'I_m) (n1 n0 : 'I_n) : n1 != n0 -> m0 != m1 -> n1 \in 'V(m0, n0) -> n1 \notin 'V(m1, n0).
proof: Proof. move=> n1n0 m0m1 Hn1; apply/negP => Hm1. have Hm0' : n0 \in 'V m0. apply: contraLR Hn1. move/Vgraph_set1 => ->; by rewrite in_set1. have Hm1' : n0 \in 'V m1. apply: contraLR Hm1. move/Vgraph_set1 => ->; by rewrite in_set1. have Hdiff : 'V(m0, n0) :\ n0 != 'V(m1, n0) :\ n0. move: m0m1; apply contra. move/eqP => abs; apply/eqP; move: abs. apply Vgraph_injective => //. apply/set0Pn; exists n1; by rewrite in_setD1 n1n0 Hn1. apply/set0Pn; exists n1; by rewrite in_setD1 n1n0 Hm1. move: (trivIset_Vgraph_part_vnode n0). move/trivIsetP. move/(_ ('V(m0, n0) :\ n0) ('V(m1, n0) :\ n0)) => /= abs. have : 'V(m0, n0) :\ n0 \in Vgraph_part_vnode n0. case: imsetP => // abs'. exfalso. apply abs'; exists m0 => //; by rewrite FnextE. move/abs => {}abs. have : 'V(m1, n0) :\ n0 \in Vgraph_part_vnode n0. case: imsetP => // abs'; exfalso. apply abs'; exists m1 => //; by rewrite FnextE. move/abs => {}abs. move: (abs Hdiff) => {abs}abs'. move/disjoint_setI0 : abs' => abs'. move: abs'; apply/eqP. apply/set0Pn. exists n1. by rewrite in_setI in_setD1 n1n0 /= Hn1 /= in_setD1 n1n0 Hm1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2