proposition: Lemma Nint_pr4 n: natp n -> ( ((Nint n) +s1 n = (Nint (csucc n))) /\ ~(inc n (Nint n))).
proof: Proof. move=> nN; rewrite {1} (NintE nN) (NintE (NS_succ nN)) (succ_of_nat nN). by split => //; case/(NintP nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)