proposition: Lemma trivIset_Vgraph_part_vnode n0 : trivIset (Vgraph_part_vnode n0).
proof: Proof. have : trivIset (subgraph_succ (tanner_rel H) (inr n0)). exact: trivIsetS _ (subsetUr _ _) (trivIset_subgraph_succ (simple_tanner_rel H) (sym_tanner_rel H) Hacyclic (inr n0)). apply: trivIsetS_f => /= z. case/imsetP => /= i Hi Hz. exists [set x | x in (subgraph (tanner_rel H) (inl i) (inr n0))]. split. apply/imsetP. exists (inl i). by rewrite inE /= -VnextE -FnextE. apply/setP => /= j. move Hlhs : (j \in _) => [|]; first by case/imsetP : Hlhs => /= k kz ->. apply/esym/negbTE. move/negbT : Hlhs; apply contra => Hlhs. apply/imsetP. by exists j. apply/setP => /= j. move Hlhs : (j \in z) => [|]. rewrite inE. apply/esym/imsetP => /=. exists (inr j) => //. rewrite Hz !inE in Hlhs. case/andP : Hlhs => jn0. case/orP => jn0'. by rewrite (negbTE jn0) in jn0'. by rewrite inE. apply/esym/negbTE. move/negbT : Hlhs; apply contra. rewrite inE. case/imsetP => /= p Hp ?; subst p. rewrite Hz !inE. apply/andP; split. apply/negP => /eqP ?; subst j. move: Hp; apply/negP. apply (root_notin_subgraph (simple_tanner_rel _)). by rewrite inE /= -VnextE -FnextE. rewrite inE in Hp. by rewrite Hp orbT. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2