proposition: Lemma big_trivIset_cond P (K : pred T) (E : T -> R) : trivIset P -> \big[op/idx]_(x in cover P | K x) E x = rhs_cond P K E.
proof: Proof. move=> tiP; rewrite (partition_big (pblock P) [in P]) -/op => /= [|x]. apply: eq_bigr => A PA; apply: eq_bigl => x; rewrite andbAC; congr (_ && _). rewrite -mem_pblock; apply/andP/idP=> [[Px /eqP <- //] | Ax]. by rewrite (def_pblock tiP PA Ax). by case/andP=> Px _; apply: pblock_mem. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)