proposition: Lemma big_trivIset P (E : T -> R) : trivIset P -> \big[op/idx]_(x in cover P) E x = rhs P E.
proof: Proof. have biginT := eq_bigl _ _ (fun _ => andbT _) => tiP. by rewrite -biginT big_trivIset_cond //; apply: eq_bigr => A _; apply: biginT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)