proposition: Lemma cpred_pr6' k i: natp k -> \1c <=c i -> i <=c k -> [/\ natp (cpred i), i = csucc (cpred i) & cpred i <c k ].
proof: Proof. move => sa sb sc. have w:= clt_01. have knz: k <> \0c by move => kz; move:(cleT sb sc); rewrite kz; apply:cltNge. move: (cpred_pr sa knz) =>[ka kb]; move: sc;rewrite kb => sc. move: (cpred_pr6 ka sb sc) => [pa pb /(cltSleP ka) pc]; split => //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)