proposition: Lemma power_big : forall x y : IR, [0] [<=] x -> [1] [<] y -> {N : nat | x [<=] y[^]N}.
proof: Proof. intros. cut ([0] [<] y[-][1]). intro. cut (y[-][1] [#] [0]). intro H2. elim (Archimedes (x[-][1][/] y[-][1][//]H2)). intro N. intros. exists N. apply leEq_transitive with ([1][+]nring N[*] (y[-][1])). apply shift_leEq_plus'. astepr ((y[-][1]) [*]nring N). apply shift_leEq_mult' with H2. auto. auto. apply leEq_wdr with (([1][+] (y[-][1])) [^]N). apply power_big'. apply less_leEq. auto. apply un_op_wd_unfolded. rational. apply Greater_imp_ap. auto. apply shift_less_minus. astepl OneR. auto. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero