proposition: Lemma nds_tn_ex_ax n: natp n -> nds_tn_ax nds_base n.
proof: Proof. move => nN; split. move => i lin; move:(NS_lt_nat lin nN) => yN. exact:(proj1 (the_cnf_omega_kj (conj (NS_pow NS2 yN) (cpow2_pos _)) yN)). exists \1o; first by apply:OS1. by move => i lin; move:(NS_lt_nat lin nN) => /nds_base_prop []. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)