proposition: Lemma CS_pred a: cardinalp a -> cardinalp (cpred a).
proof: Proof. move => h; case: (Nat_dichot h); first by move/NS_pred/CS_nat. by move/(cpred_inf) => ->. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)