proposition: Lemma big_trivIfset P (E : T -> R) : trivIfset P -> \big[op/idx]_(x <- fcover P) E x = rhs P E.
proof: Proof. rewrite /rhs /fcover => /trivIfsetP tI. have {tI} : {in enum_fset P &, forall A B, A != B -> [disjoint A & B]%fset}. by []. elim: (enum_fset P) (fset_uniq P) => [_|h t ih /= /andP[ht ut] tP]. by rewrite !big_nil. rewrite !big_cons -ih //; last first. by move=> x y xt yt xy; apply tP => //; rewrite !inE ?(xt,yt) orbT. rewrite {1}/fsetU big_imfset //= undup_cat /= big_cat !undup_id //. congr (op _ _). suff : [seq x <- h | x \notin (\bigcup_(j <- t) j)%fset] = h by move=>->. rewrite -[RHS]filter_predT; apply eq_in_filter => x xh. apply/negP/idP; apply/negP => /bigfcupP[/= A]. rewrite andbT => At xA. have hA : h != A by move/negP : ht => /negP; apply: contra => /eqP ->. move: (tP h A). rewrite !inE eqxx => /(_ erefl); rewrite At orbT => /(_ erefl hA). by rewrite -fsetI_eq0 => /eqP /fsetP /(_ x); rewrite !inE xh xA. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrnat eqtype ssrfun seq) mathcomp(choice path finset finfun fintype bigop)