proposition: Lemma card_Nintc a: natp a -> cardinal (Nintc a) = csucc a.
proof: Proof. by move => aN; rewrite (NintcE aN) (card_card (CS_succ _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)