proposition: Lemma cdiffSn a b: natp a -> b <=c a -> (csucc a) -c b = csucc (a -c b).
proof: Proof. move => aN leab. rewrite (Nsucc_rw aN) (Nsucc_rw (NS_diff b aN)); apply: (cdiffA2 aN NS1 leab). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)