proposition: Lemma NintsP a: natp a -> forall x, (inc x (Nint (csucc a)) <-> x <=c a).
proof: Proof. move=> aN; rewrite - (Nint_co_cc aN); exact (NintcP aN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)