proposition: Lemma cprodA_setU2 A B f: disjoint A B -> cprodb (A \cup B) f = cprodb A f *c cprodb B f.
proof: Proof. move => /(partition_setU2 f) dab; rewrite /cprodb. rewrite (cprod_An dab) variantLc_d cprod2_pr0; aw. apply: f_equal2; apply: cprodb_exten => i ia;rewrite LgV; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)