proposition: Lemma big_fsetU (A B : {fset T}) F : [disjoint A & B] -> \big[op/idx]_(j : A `|` B) F (val j) = op (\big[op/idx]_(j : A) F (val j)) (\big[op/idx]_(j : B) F (val j)).
proof: Proof. move=> dj_AB; rewrite !big_fset_seq -big_cat; apply/perm_big. apply/uniq_perm=> //. + rewrite cat_uniq ?uniq_fset_keys !(andbT, andTb); apply/hasPn => x /=. by apply/fdisjointP; rewrite fdisjoint_sym. + by move=> x; rewrite mem_cat in_fsetE. Qed.
imports: mathcomp(all_ssreflect all_algebra)