proposition: Lemma cover_Fgraph_part_Fgraph m0 n0 : n0 \in 'V m0 -> cover (Fgraph_part_Fgraph m0 n0) = 'F(m0, n0) :\ m0.
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 => /= m1. rewrite 2!inE. move Hlhs : ( _ \in _ ) => [|]. apply/esym. have Hm1 : inl m1 \in cover (subgraph_succ2_D1 m0n0). rewrite /Fgraph_part_Fgraph 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 /=. apply/bigcupP => /=. rewrite i1 in i2. case/bigcupP : i2 => /= m2 Hm2 Hm1. exists (inl m2). rewrite !inE /=. rewrite !inE /= in Hm1. case/andP : Hm1 => -> _; rewrite andbT. apply/eqP => abs; case : abs => ?; subst m2. by rewrite !inE /= eqxx in Hm2. rewrite !inE /= in Hm1. by rewrite /subgraph !inE. rewrite Hcover 2!inE in Hm1. apply/andP; split. case/andP : Hm1 => Hm1 _. by apply: contra Hm1 => /eqP ->. case/andP : Hm1 => _ Hm1. by rewrite inE. apply/esym/negbTE. rewrite negb_and negbK. case/boolP : (m1 == m0) => // m1m0 /=. move/negbT : Hlhs; apply contra => Hlhs. apply/bigcupP => /=. rewrite inE in Hlhs. rewrite /Fgraph_part_Fgraph. rewrite !inE /= in Hlhs. case/andP : Hlhs => Hlhs Hlhs'. case/connectP : Hlhs' => /= p. case/shortenP => p' Hp' Hun p'p Hlast. case: p' Hp' Hun p'p Hlast => [|p1 p2] Hp' Hun p'p Hlast. rewrite /= in Hlast. case: Hlast => ?; subst m1. by rewrite eqxx in m1m0. case: p1 Hp' Hun p'p Hlast => [|n1 Hp' Hun p'p Hlast]. by rewrite exceptE /= tanner_relE. exists (\bigcup_(m2 in 'F n1 :\ m0) 'F(m2, n1)). apply/imsetP. exists n1 => //. rewrite !inE. rewrite /= in Hp'. case/andP : Hp'. rewrite {1}exceptE /= -VnextE => /andP[H1 H2] _. rewrite H1 andbT. by apply: contra H2 => /eqP ->. apply/bigcupP => /=. case: p2 Hp' Hun p'p Hlast => [ // | [p2|p2] p'] Hp' Hun p'p Hlast; last first. by rewrite exceptE /= tanner_relE /= andbF in Hp'. rewrite /= in Hp'. case/andP : Hp' => H1 /andP [] H2 H3. exists p2. rewrite !inE. apply/andP; split. apply/eqP => ?; subst p2. rewrite -(cat1s (inl m0)) -(cat1s (inr n1)) -[in X in _ ++ X](cat1s (inl m0)) in Hun. by rewrite catA uniq_catCA /= inE eqxx /= in Hun. by move/except_rel : H2; rewrite /= -VnextE -FnextE. rewrite !inE. rewrite (except_rel H2) /=. apply/connectP; exists p' => //. apply: sub_path_except H3 => //. apply/negP => n1p'. move: Hun. rewrite -(cat1s (inl m0)) -(cat1s (inr n1)) -(cat1s (inl p2)) catA uniq_catCA. by rewrite catA uniq_catC -!catA catA cat_uniq uniq_catC /= n1p'. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2