proposition: Lemma cprodA_setU1 A b f: ~ (inc b A) -> cprodb (A +s1 b) f = cprodb A f *c (f b).
proof: Proof. move => /disjoint_setU1 pc. by rewrite - cprod2cr (cprodA_setU2 _ pc) - cprod_trivial3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)