proposition: Lemma cdiff_lt_pred a b: natp b -> b <> \0c -> (a <c b <-> a <=c (b -c \1c)).
proof: Proof. move => bN /(cpred_pr bN) [sa sb]. rewrite - (cpred_pr4 (CS_nat bN)) {1} sb;exact:(cltSleP sa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)