proposition: Lemma Nint_pr5 n (si := Nintcc \1c n): natp n -> ( (si +s1 \0c = Nintc n) /\ ~(inc \0c si)).
proof: Proof. move=> nN; split. set_extens x. case /setU1_P; first by move /(Nint_ccP1 NS1 nN) => [_]/(NintcP nN). move => ->; apply /(NintcP nN); exact: (cle0n nN). move /(NintcP nN) => h; apply /setU1_P. case: (equal_or_not x \0c) => xz; [ by right | left ]. apply /(Nint_ccP1 NS1 nN);split => //;apply: cge1 => //; exact: (proj31 h). move /(Nint_ccP1 NS1 nN) => [ /cleNgt []]; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)