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