proposition: Lemma nds_small_base i: natp i -> nds_small_nz (nds_base i).
proof: Proof. move => iN. move: (proj31 (nds_base_prop iN)) => dx. move: (proj1 (nds_tn_ex_ax (NS_succ iN)) i (cltS iN)) => bp; split => //. move: (proj2 (the_cnf_p4 bp)); rewrite dx => h; apply: (olt_leT h). apply: (opow_Mo_le); rewrite osucc_one; apply: ole_2omega. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)