proposition: Lemma csum2_compare_spec a b s : natp a -> natp b -> s = a +c b -> a <=c s /\ (a = s -> b = \0c).
proof: Proof. move => aN bN ->; split. exact: (csum_M0le b (CS_nat aN)). by rewrite -{1}(csum0r (CS_nat aN)); move/(csum_eq2l aN NS0 bN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)