proposition: Lemma NintE n: natp n -> Nint n = n.
proof: Proof. move=> nN; have h := (Nint_coP1 NS0 nN). set_extens t; first by move/h => [_ /(NltP nN)]. move/(NltP nN)=> ltn; apply/h; split => //;apply: (cle0x (proj31_1 ltn)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)