proposition: Lemma cover_Vgraph_part_vnode (n0 : 'I_n) : cover (Vgraph_part_vnode n0) = setT :\ n0.
proof: Proof. apply/setP => /= n1. rewrite !inE andbT. case/boolP : (n1 == n0) => [ /eqP -> | n1n0] /=. exact/negbTE/notin_Vgraph_part_vnode. apply/bigcupP => /=. have : inr n1 \in cover ([set inr n0] |: subgraph_succ (tanner_rel H) (inr n0)). by rewrite (cover_subgraph_succ (tanner_rel H) (inr n0)) inE Hconnect. case/bigcupP => /= p. rewrite !inE. case/orP => [ /eqP -> | ]. rewrite inE. case/eqP => abs; by rewrite abs eqxx in n1n0. case/imsetP => /=; case=> p1; last by rewrite inE tanner_relE. move=> Hp1 pp1 n1p. exists ('V(p1, n0) :\ n0). apply/imsetP => /=. exists p1 => //. rewrite inE /= -VnextE in Hp1. by rewrite FnextE. rewrite !inE n1n0 /= predU1r //. by rewrite pp1 inE in n1p. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2