proposition: Theorem succ_injective a b: cardinalp a -> cardinalp b -> a +c \1c = b +c \1c -> a = b.
proof: Proof. move=> ca cb; rewrite - (csucc_pr4 ca)- (csucc_pr4 cb). by apply: csucc_inj. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)