proposition: Lemma nds_card_0 X: nds_card X \0c = \1c.
proof: Proof. apply: cleA. by move: (nds_card_bd X NS0); rewrite factorial0. by apply/cle1P; apply:funI_setne; exists (identity \0c); apply:permutation_id. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)