proposition: Lemma nds_of_nat n X: natp n -> (forall i, i <c n -> natp (X i)) -> nds_card X n = \1c.
proof: Proof. move => nN Xp. suff: (nds_sums X n) = singleton (osumf X n). by rewrite /nds_card;move => ->; rewrite cardinal_set1. apply: set1_pr1. move:(permutation_id n) => ip; apply/funI_setne; ex_tac. move => s/funI_P [z zp ->]; exact:osum_of_nat_bis. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)