proposition: Lemma cover_Vgraph_part_Vgraph m0 n0 : n0 \in 'V m0 -> cover (Vgraph_part_Vgraph m0 n0) = 'V(m0, n0) :\ n0.
proof: Proof. move=> Hn0. have {Hn0}m0n0 : tanner_rel H (inl m0) (inr n0) by rewrite VnextE sym_tanner_rel in Hn0. move: (cover_subgraph_succ2_D1 (sym_tanner_rel H) Hacyclic (simple_tanner_rel H) m0n0) => Hcover. apply/setP => /= n1. rewrite 2!inE. move Hlhs : ( _ \in _ ) => [|]. apply/esym. have Hn1 : inr n1 \in cover (subgraph_succ2_D1 m0n0). rewrite /Vgraph_part_Vgraph in Hlhs. case/bigcupP : Hlhs => /= i i1 i2. case/imsetP : i1 => /= n1' Hn1' i1. apply/bigcupP => /=. exists (inr n1' |: \bigcup_(m' in successors (tanner_rel H) (inr n1') :\ inl m0) (subgraph (tanner_rel H) m' (inr n1'))). apply/imsetP => /=. exists (inr n1') => //. rewrite !inE /= -VnextE. rewrite !inE /= in Hn1'. case/andP: Hn1' => Hn1' ->; rewrite andbT. by apply: contra Hn1' => /eqP Hn1'; case: Hn1' => ->. rewrite !inE /=. rewrite i1 !inE in i2. case/orP : i2. move/eqP => ->; by rewrite eqxx. case/bigcupP => /= m1 Hm1. rewrite in_setD1. case/andP => n1n1' Hn1. apply/orP; right. apply/bigcupP => /=. exists (inl m1). move: Hm1. rewrite in_setD1 /= in_setD1 inE /= -VnextE -FnextE. case/andP => Hm1 ->; rewrite andbT. by apply: contra Hm1 => /eqP [] ->. by rewrite inE in_set1 (negbTE n1n1') /= inE in Hn1. move: Hn1. rewrite Hcover in_setD1. case/andP => n1m0 Hn1. apply/andP; split. apply/eqP => ?; subst n1. move: Hn1. apply/negP/(root_notin_subgraph (simple_tanner_rel _)). by rewrite inE sym_tanner_rel. by rewrite 3!inE Hn1 orbT. apply/esym/negbTE. move/negbT : Hlhs; apply contra. case/andP. rewrite 2!inE. move=> n1n0. rewrite in_set1 (negbTE n1n0) orFb. rewrite inE. case/andP => _ Hn1. apply/bigcupP => /=. case/connectP : Hn1 => /= p. case/shortenP. case=> //. case=> [|n2 p' Hp' Hun p'p Hlast]; first by rewrite exceptE tanner_relE. exists (n2 |: \bigcup_(m1 in 'F n2 :\ m0) ('V(m1, n2) :\ n2)). apply/imsetP => /=. exists n2 => //. rewrite !inE /=. move: Hp'. rewrite /= exceptE /= -VnextE -andbA => /and3P[] -> tmp _. rewrite andbT. by apply: contra tmp => /eqP ->. rewrite !inE. case: (boolP (n1 == n2)) => //= n1n2. apply/bigcupP. case: p' Hp' Hun p'p Hlast => //. move=> _ _ _ [] ?; subst n2; by rewrite eqxx in n1n2. case; last by rewrite exceptE /= tanner_relE /= andbF. move=> m1 p' Hp' Hun p'p Hlast. rewrite /= in Hp'. case/andP : Hp' => H1 /andP [] H2 H3. rewrite exceptE /= andbT -VnextE -FnextE in H2. exists m1. rewrite !inE. case/andP : H2 => -> _. rewrite -(cat1s (inl m0)) -(cat1s (inr n2)) -(cat1s (inl m1)) in Hun. rewrite uniq_catCA uniq_catC /= in Hun. case/andP : Hun. rewrite inE negb_or. case/andP => Hun _ _. rewrite andbT. by apply: contra Hun => /eqP ->. rewrite !inE (negbTE n1n2) /= -VnextE -FnextE. case/andP : H2 => -> H2 /=. apply/connectP; exists p' => //. apply: sub_path_except H3 => //. apply/negP => n2p'. move: Hun. rewrite -(cat1s (inl m0)) -(cat1s (inr n2)) -(cat1s (inl m1)) catA uniq_catCA. by rewrite catA uniq_catC -!catA catA cat_uniq uniq_catC /= n2p'. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2