proposition: Lemma nds_C_prop n a: natp n -> inc a n -> cardinal (\Po (n -s1 a)) = \2c ^c (cpred n).
proof: Proof. move => mN an. case: (equal_or_not n \0c) => mp; first by move: an; rewrite mp => /in_set0. move:(cpred_pr mN mp) => [pnN pnv]. have ->: cpred n = cardinal (n -s1 a). by apply:csucc_inj;fprops;rewrite - pnv - (csucc_pr2 an) (card_nat mN). by rewrite cpowcr - card_setP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)