proposition: Lemma cpred_pr1 n: cardinalp n -> cpred (csucc n) = n.
proof: Proof. case /Nat_dichot; first by move/cpred_pr2. by move => ifn;move: (ifn) => /csucc_inf <-; apply: cpred_inf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)