proposition: Lemma NintcP b: natp b -> forall x, inc x (Nintc b) <-> x <=c b.
proof: Proof. move=> bN x; split; first by move /Nint_ccP => [_ [_ _ h]]. by move => h;apply /(Nint_ccP1 NS0 bN); move: (cle0x (proj31 h)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)