proposition: Lemma cpred_lt n: natp n -> n <> \0c -> cpred n <c n.
proof: Proof. move => nN nz. move: (cpred_pr nN nz) =>[sa sb]. apply /(cleSltP sa); rewrite - sb; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)