proposition: Lemma trivIset_Vgraph_part_Vgraph m0 n0 : n0 \in 'V m0 -> trivIset (Vgraph_part_Vgraph m0 n0).
proof: Proof. move=> m0n0. have {}m0n0 : tanner_rel H (inl m0) (inr n0) by rewrite VnextE sym_tanner_rel in m0n0. move: (@trivIset_subgraph_succ2_D1 _ _ (sym_tanner_rel H) Hacyclic (simple_tanner_rel _) (inl m0) (inr n0) m0n0) => K. apply: (@trivIsetS_f _ _ inr) K => /= z. rewrite /Vgraph_part_Vgraph. case/imsetP => /= n1 Hn1 Hz. rewrite /subgraph_succ2_D1. exists (inr n1 |: \bigcup_(m1 in successors (tanner_rel H) (inr n1) :\ inl m0) (@subgraph _ (tanner_rel H) m1 (inr n1))). split. apply/imsetP => /=. exists (inr n1) => //. rewrite !inE /= in Hn1. rewrite !inE /= -VnextE. case/andP : Hn1 => Hn1 ->. rewrite andbT. by apply: contra Hn1 => /eqP [] ->. rewrite Hz. apply/setP => /= m1. rewrite !inE. case: (boolP (m1 == n1)) => [|m1n1] /=. move/eqP => ->; by rewrite eqxx. rewrite (_ : inr m1 == _ = false) /=; last first. apply/negbTE. by apply: contra m1n1 => /eqP [] ->. apply/bigcupP. case: ifP. case/bigcupP => /=. case => [m2 | n2]; last by rewrite !inE {2}tanner_relE. rewrite 3!inE /=. case/andP => m2m0 m2n1 X. rewrite -VnextE -FnextE in m2n1. exists m2. rewrite !inE /= m2n1 andbT. by apply: contra m2m0 => /eqP ->. by rewrite in_setD1 m1n1 /= inE in_set1 (negbTE m1n1) orFb inE. move/bigcupP => abs abs'; apply abs => {abs}. case: abs' => m2 Hm2 Hm1 /=. exists (inl m2). rewrite !inE /= -VnextE -FnextE. rewrite !inE /= in Hm2. case/andP : Hm2 => m2m0 ->. rewrite andbT. by apply: contra m2m0 => /eqP [] ->. rewrite !inE (negbTE m1n1) /= in Hm1. by rewrite !inE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2