proposition: Lemma cdiff_A1 a b: natp a -> natp b -> (csucc b) <=c a -> cpred (a -c b) = a -c (csucc b).
proof: Proof. move=> aN bN; rewrite (Nsucc_rw bN) => h'. rewrite - cdiffA; fprops; apply: cpred_pr4; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)