proposition: Theorem finite_succP x: cardinalp x -> (finite_c (csucc x) <-> finite_c x).
proof: Proof. case /finite_or_infinite. move => h; rewrite (succ_of_finite h); exact: finite_sP. by move /csucc_inf => <-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)