proposition: Lemma NintP a: natp a -> forall x, (inc x (Nint a) <-> x <c a).
proof: Proof. by move=> aN x; rewrite (NintE aN); apply: iff_sym;apply: NltP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)