proposition: Lemma Nint1cP b: natp b -> forall x, inc x (Nint1c b) <-> (x <> \0c /\ x <=c b).
proof: Proof. move=> bN x; apply: (iff_trans (Nint_ccP1 NS1 bN x)). split; move => [pa pb]; split => //. exact: (nesym (proj2 (clt_leT clt_01 pa))). exact: (cge1 (proj31 pb) pa). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)