proposition: Lemma csum_eq1 a b: cardinalp a -> cardinalp b -> a +c b = \1c -> (a = \0c \/ b = \0c).
proof: Proof. move => ca cb eq. case: (equal_or_not a \0c) => anz; first by left. case: (equal_or_not b \0c) => bnz; first by right. move:(csum_Mlele (cge1 ca anz) (cge1 cb bnz)). by rewrite csum_11 eq => /(cltNge clt_12). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)