proposition: Theorem nds_alt_som n: natp n -> nds_F n = nds_sol n.
proof: Proof. have F0: nds_F \0c = \1c. by move: (proj43 (nds_f_def NS0)) => [X _ <-]; rewrite (nds_card_0 X). have F1: nds_F \1c = \1c. by move: (proj43 (nds_f_def NS1)) => [X _ <-]; rewrite (nds_card_1 X). move:n; apply: nds_alt => //. apply: nds_alt_prop1. move => n nN. have sp: (\1c <=c csucc n) by rewrite - succ_zero; apply/cleSS; apply: cle0n. move: (nds_card_sol (NS_succ nN) sp) => [xa xn]. by move: (proj44 (nds_f_def (NS_succ nN)) _ xa); rewrite xn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)