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