proposition: Lemma nds_card_sol (X:= nds_example) n: natp n -> \1c <=c n -> nds_ax (X n) n /\ nds_sol n = nds_card (X n) n.
proof: Proof. move => nN np. split. by move => i lin; move: (nds_example_small_ax nN lin) => [/proj32_1]. symmetry; clear np; move: n nN; apply: nds_k_of_prop. - by rewrite(@nds_card_0 (X \0c)). - by rewrite(@nds_card_1 (X \1c)). - move => n nN ng1. move: (proj33 nds_induction_prop2 _ nN ng1); simpl. move: (nds_k_of_bd nN ng1). set k := (nds_k_of n); move => [lk0 kln] hr. move: (NS_diff k nN) => dkN. have w: opos_below (X (n -c k)) (n -c k). by move => i /(nds_example_small_ax dkN) /proj1. rewrite - (nds_card_merge nN kln w). by apply: (nds_card_exten nN). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)