proposition: Lemma cpred_pr6 k i: natp k -> \1c <=c i -> i <=c csucc k -> [/\ natp (cpred i), i = csucc (cpred i) & cpred i <=c k].
proof: Proof. move => kN sa sb. have inz : i <> \0c by move => iz; case:(cltNge clt_01); rewrite -iz. move: (cpred_pr (NS_le_nat sb (NS_succ kN)) inz) => [ra rb]; split => //. by move: sb; rewrite {1} rb; move /(cleSSP (CS_nat ra)( (CS_nat kN))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)