proposition: Lemma set_partition_big P D (E : T -> R) : partition P D -> \big[op/idx]_(x in D) E x = rhs P E.
proof: Proof. by case/and3P=> /eqP <- tI_P _; apply: big_trivIset. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)