proposition: Lemma trivIset_Fgraph_part_fnode (n0 : 'I_n) : trivIset (Fgraph_part_fnode n0).
proof: Proof. have K : trivIset (subgraph_succ (tanner_rel H) (inr n0)). exact: trivIsetS _ (subsetUr _ _) (trivIset_subgraph_succ (simple_tanner_rel H) (sym_tanner_rel H) Hacyclic (inr n0)). apply: trivIsetS_f K => /= z. case/imsetP => /= i Hi Hz. exists [set x | x in subgraph (tanner_rel H) (inl i) (inr n0)]. split. apply/imsetP. exists (inl i). by rewrite inE /= -VnextE -FnextE. apply/setP => /= j. move Hlhs : (j \in _) => [|]; first by case/imsetP : Hlhs => /= k kz ->. apply/esym/negbTE. move/negbT : Hlhs; apply contra => Hlhs. apply/imsetP. by exists j. apply/setP => /= j. rewrite inE. move Hlhs : (j \in z) => [|]. apply/esym/imsetP. exists (inl j) => //. by rewrite Hz /Fgraph inE in Hlhs. apply/esym/negbTE. move/negbT : Hlhs; apply contra. case/imsetP => /= p Hp ?; subst p. by rewrite Hz inE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2