proposition: Lemma trivIset_Fgraph_part_Fgraph m0 n0 : n0 \in 'V m0 -> trivIset (Fgraph_part_Fgraph m0 n0).
proof: Proof. move=> m0n0. rewrite VnextE sym_tanner_rel in m0n0. move: (@trivIset_subgraph_succ2_D1 _ _ (sym_tanner_rel H) Hacyclic (simple_tanner_rel H) (inl m0) (inr n0) m0n0) => K. apply: (@trivIsetS_f _ _ inl) K => /= z. rewrite /Fgraph_part_Fgraph. case/imsetP => n1 Hn1 Hz. rewrite /subgraph_succ2_D1. exists (inr n1 |: \bigcup_(m1 in successors (tanner_rel H) (inr n1) :\ inl m0) (subgraph (tanner_rel H) m1 (inr n1))). split. apply/imsetP => /=. exists (inr n1). rewrite !inE /= in Hn1. rewrite !inE /= -VnextE. case/andP : Hn1 => Hn1 ->. rewrite andbT. by apply: contra Hn1 => /eqP [] ->. by f_equal. rewrite Hz. apply/setP => /= m1. apply/bigcupP. case: ifP. rewrite 3!inE /=. case/bigcupP => /=. case=> [m2 Hm2 Hm1 | n2]. exists m2 => //. rewrite in_setD1 FnextE. rewrite !inE /= -VnextE in Hm2. case/andP : Hm2 => Hm2 ->. rewrite andbT. by apply: contra Hm2 => /eqP ->. by rewrite inE. by rewrite !inE {2}tanner_relE. rewrite !inE /=. move/negbT/negP => abs' abs; apply abs' => {abs'}. case: abs => m2 Hm Hm1. apply/bigcupP => /=. exists (inl m2). rewrite !inE /= -VnextE. rewrite in_setD1 FnextE in Hm. case/andP : Hm => Hm ->. rewrite andbT. by apply: contra Hm => /eqP [] ->. by rewrite inE in Hm1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2