proposition: Lemma Nint_M a: natp a -> sub (Nint a) (Nint (csucc a)).
proof: Proof. move => aN; rewrite (NintE aN) (NintE (NS_succ aN)) (succ_of_nat aN). apply:subsetU2l. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)