proposition: Lemma card_Nintcp a: natp a -> a <> \0c -> cardinal (Nintc (cpred a)) = a.
proof: Proof. move=> aN naz. by move: (cpred_pr aN naz) => [fp ass]; rewrite card_Nintc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)