proposition: Lemma partition_big_nodes_arities {A : finType} (f : {set A} -> K) (P : pred {set A}): \sum_(x | P x) f x = \sum_(j < #|A|.+1) \sum_(i : {set A} | P i && (#|i| == j)) f i.
proof: Proof. rewrite (@partition_big _ _ _ _ _ _ P (fun pn => nth ord0 (enum 'I_#|A|.+1) #|pn|) predT) //=. apply eq_bigr => j _; apply eq_bigl => x. have x_ub : (#|x| < #|A|.+1)%nat by rewrite ltnS; apply max_card. by rewrite (@nth_ord_enum #|A|.+1 ord0 (Ordinal x_ub)). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner