proposition: Lemma cover_Fgraph_part_fnode (n0 : 'I_n) : cover (Fgraph_part_fnode n0) = setT.
proof: Proof. apply/setP => /= m1; rewrite in_set. apply/bigcupP => /=. have : inl m1 \in cover ([set inr n0] |: subgraph_succ (tanner_rel H) (inr n0)). move: (cover_subgraph_succ (tanner_rel H) (inr n0)) => /setP/(_ (inl m1)) ->. by rewrite inE Hconnect. case/bigcupP => /= E HE m1_in_E. rewrite in_setU1 in HE. move/orP: HE => [HE | ]. by rewrite (eqP HE) in_set1 in m1_in_E. case/imsetP => /= p Hp HE. rewrite HE in_set in m1_in_E. rewrite in_set in Hp. case: p HE Hp m1_in_E => p HE /= Hp m1_in_E; last by rewrite tanner_relE in m1_in_E. exists [set m0 | inl m0 \in E]. apply/imsetP => /=. exists p. by rewrite FnextE VnextE. apply/setP => /= m0. by rewrite HE !inE. by rewrite HE !in_set. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2