proposition: Lemma csumA_setU1 A b f: ~ (inc b A) -> csumb (A +s1 b) f = csumb A f +c (f b).
proof: Proof. move => /disjoint_setU1 pa. by rewrite -csum2cr (csumA_setU2 _ pa) csum_trivial3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)