proposition: Lemma incsx_intsn x n: natp n -> inc x (Nint n) -> inc (csucc x) (Nint (csucc n)).
proof: Proof. by move => nN; move/(NintP nN) => /cltSS /(NintP (NS_succ nN)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)