proposition: Lemma NS_pred a: natp a -> natp (cpred a).
proof: Proof. move => aN; case: (equal_or_not a \0c) => az. by rewrite az cpred0 -az. exact: (proj1 (cpred_pr aN az)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)