proposition: Lemma notin_Vgraph n1 m0 n0 m1 : n0 \in 'V m0 -> n1 \in 'V m0 :\ n0 -> m1 \in 'F n1 :\ m0 -> n0 \notin 'V(m1, n1).
proof: Proof. move=> n0m0 Hn1 Hm1. rewrite in_setD1 in Hn1; case/andP : Hn1 => n1n0 n1m0. rewrite in_setD1 in Hm1; case/andP : Hm1 => m1m0 m1n1. suff : inr n0 \notin subgraph (tanner_rel H) (inl m1) (inr n1). move=> ?. by rewrite /Vgraph inE negb_or in_set1 eq_sym n1n0 /= inE. apply: (@notin_subgraph _ (tanner_rel H) _ _ _ _ (inl m0)) => //. exact: sym_tanner_rel. exact: simple_tanner_rel. by rewrite /= -VnextE. by rewrite /= -VnextE. by rewrite /= -VnextE -FnextE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2