proposition: Lemma Nint1cPb b: natp b -> forall x, (inc x (Nint1c b) <-> (\1c <=c x /\ x <=c b)).
proof: Proof. move=> aN x; apply: (Nint_ccP1 NS1 aN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)