proposition: Lemma card_Nint1c a: natp a -> cardinal (Nint1c a) = a.
proof: Proof. move => aN. case: (equal_or_not a \0c) => anz. have aux: (Nint1c \0c = emptyset). apply /set0_P => y; move /(Nint1cPb NS0)=> [c1y cy0]. exact: (cleNgt (cleT c1y cy0) clt_01). rewrite anz aux; apply: cardinal_set0. have aux1: \1c <=c a by apply: cge1; fprops. have aux: \1c <=N a by split;fprops. have so:= (NS_diff \1c aN). by rewrite card_Nintcc // Nsucc_rw // csumC; apply: cdiff_pr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(binomial div)