proposition: Lemma nexp_resp_Two : forall x : R1, [1][<]x -> {M : nat | Two[<]x[^]M}.
proof: Proof. intros. cut (x[-][1][#][0]). intro H0. cut {N : nat | ([1][/] x[-][1][//]H0)[<]nring N}. intro H1. case H1. intro N. intro. exists (S N). apply less_transitive_unfolded with (y := (([1][/] nring (S N)[//]nringS_ap_zero _ N)[+]([1]:R1))[^]S N). apply less_wdl with (x := ([1]:R1)[+] nring (S N)[*]([1][/] nring (S N)[//]nringS_ap_zero _ N)). apply very_weak_binomial. apply recip_resp_pos. apply pos_nring_S. apply -> Nat.succ_lt_mono. apply Nat.neq_0_lt_0. apply Nat.neq_sym. apply (nring_ap_zero_imp R1). apply Greater_imp_ap. apply less_transitive_unfolded with (y := [1][/] x[-][1][//]H0). apply recip_resp_pos. apply shift_zero_less_minus. assumption. assumption. rational. apply nexp_resp_less. apply le_n_S. apply Nat.le_0_l. apply less_leEq. apply less_transitive_unfolded with (y := [1]:R1). apply pos_one. apply plus_cancel_less with (z := [--]([1]:R1)). astepl ([0]:R1). rstepr (([1]:R1)[/] nring (S N)[//]nringS_ap_zero R1 N). apply recip_resp_pos. apply pos_nring_S. apply plus_cancel_less with (z := [--]([1]:R1)). rstepl ([1][/] nring (S N)[//]nringS_ap_zero R1 N). astepr (x[-][1]). apply swap_div with (z_ := H0). apply pos_nring_S. apply shift_zero_less_minus. assumption. apply less_transitive_unfolded with (y := nring (R:=R1) N). assumption. apply nring_less_succ. apply Archimedes'. apply Greater_imp_ap. apply shift_zero_less_minus. assumption. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon