proposition: Lemma nds_example_small_ax n: natp n -> nds_small_ax (nds_example n) n.
proof: Proof. move: nds_induction_prop2 => [qa qb qc]. move => nN; move: {1 3 4}(n) (cleR (CS_nat nN)). move: n nN; apply:Nat_induction. by move => m /cle0 -> i /clt0. move => m mN Hrec q /cle_eqVlt; case => qv; last first. by move /(cltSleP mN):qv => /Hrec. rewrite qv; case: (czero_dichot (CS_nat mN)) => mz. rewrite mz succ_zero => i iN; rewrite (qb _ (NS_lt_nat iN NS1)). split; first by apply: olt_01. by rewrite - oopow0; apply: opow_Mo_lt; apply: olt_0omega. have sp: \1c <c csucc m by rewrite - succ_zero; exact: (cltSS mz). move: (NS_succ mN) => sN i lin. move: (NS_lt_nat lin sN) => iN. move: (nds_k_of_bd sN sp). rewrite (qc _ sN sp i lin); set k := nds_k_of _; move => [kp lkm]. move: (NS_lt_nat lkm sN) => kN. rewrite/nds_merge. case: (NleT_el kN iN) => cik; last by Ytac0; apply:nds_small_base. have ha: (csucc m -c k) <=c m. apply/(cltSleP mN);apply: (cdiff_ltb sN (proj1 lkm) (nesym (proj2 kp))). have hb:=(cdiff_pr7 cik lin sN). rewrite (Y_false (cleNgt cik)); exact:(nds_small_nz_shift (Hrec _ ha _ hb)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)