proposition: Lemma nds_binomp_base i: natp i -> nds_binomp (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. move: (proj2 (the_cnf_p4 bp)); rewrite dx => h; apply: (olt_leT h). rewrite osucc_one; apply: oleR; apply: (OS_oopow OS2). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)