proposition: Lemma twisted_archimedean : forall (n : nat) (x : R1), [1][<]x -> {M : nat | nring n[<]x[^]M}.
proof: Proof. intros n x H. induction n as [| n Hrecn]. exists 0. simpl in |- *. apply pos_one. case Hrecn. intro M1. intros. case (nexp_resp_Two x H). intro M2. intros. exists (M1 + M2). apply less_transitive_unfolded with (y := x[^]M1[+][1]). simpl in |- *. apply plus_resp_less_leEq. assumption. apply leEq_reflexive. apply less_wdr with (y := x[^]M1[*]x[^]M2). apply plus_cancel_less with (z := [--](x[^]M1)). apply less_wdl with (x := [1]:R1). apply less_wdr with (y := x[^]M1[*](x[^]M2[-][1])). apply leEq_less_trans with (y := x[^]M1[*][1]). astepr (x[^]M1). apply nexp_resp_great_One. assumption. apply mult_resp_less_lft. apply shift_less_minus. rstepl (Two:R1). assumption. apply leEq_less_trans with (y := nring (R:=R1) n). change (nring (R:=R1) 0[<=]nring n) in |- *. apply nring_leEq. apply Nat.le_0_l. assumption. rational. rational. apply nexp_plus. Qed.
imports: CoRN.reals.iso_CReals CoRN.algebra.Expon