proposition: Lemma cpred_pr n: natp n -> n <> \0c -> (natp (cpred n) /\ n = csucc (cpred n)).
proof: Proof. move=>/NatP nN nz; move: (finite_pred nN nz) => [y /NatP yN ->]. by rewrite /cpred (succo_K (OS_nat yN)) (succ_of_nat yN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)