proposition: Lemma rprod_Fgraph_part_fnode g n0: \prod_(m0 < m) g m0 = \prod_(m0 in 'F n0) \prod_(m1 in 'F(m0, n0)) g m1 :> Rdefinitions.R.
proof: Proof. transitivity (\prod_(m0 in [set: 'I_m]) g m0). apply eq_bigl => /= ?; by rewrite in_set. rewrite -(cover_Fgraph_part_fnode n0). rewrite big_trivIset /=; last exact: trivIset_Fgraph_part_fnode. rewrite big_imset // => //. move=> m1 m2 Hm1 Hm2 /=. apply Fgraph_injective => //; by rewrite -FnextE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2