proposition: Lemma qi_yields_zero : forall q : IR, [0] [<=] q -> q [<] [1] -> forall e, [0] [<] e -> {N : nat | q[^]N [<=] e}.
proof: Proof. intros. cut ([0] [<] ([1][+]q) [/]TwoNZ). intro Haux. cut (([1][+]q) [/]TwoNZ [#] [0]). intro H2. cut (e [#] [0]). intro H3. elim (power_big ([1][/] e[//]H3) ([1][/] _[//]H2)). intro N. intros H4. exists N. cut ([0] [<] (([1][+]q) [/]TwoNZ) [^]N). intro H5. apply leEq_transitive with ((([1][+]q) [/]TwoNZ) [^]N). apply nexp_resp_leEq. auto. apply shift_leEq_div. apply pos_two. apply shift_leEq_plus. rstepl q. apply less_leEq. auto. astepl ([1][*] (([1][+]q) [/]TwoNZ) [^]N). set (H6 := pos_ap_zero _ _ H5) in *. apply shift_mult_leEq with H6. auto. rstepr (e[*] ([1][/] _[//]H6)). apply shift_leEq_mult' with H3. auto. astepr ([1][^]N[/] _[//]H6). astepr (([1][/] _[//]H2) [^]N). auto. apply nexp_resp_pos. apply pos_div_two. astepl ([0][+]ZeroR). apply plus_resp_less_leEq. apply pos_one. auto. apply less_leEq. apply recip_resp_pos. auto. apply shift_less_div. apply pos_div_two. astepl ([0][+]ZeroR). apply plus_resp_less_leEq. apply pos_one. auto. astepl (([1][+]q) [/]TwoNZ). apply shift_div_less. apply pos_two. rstepr ([1][+]OneR). apply plus_resp_less_lft. auto. apply Greater_imp_ap. auto. apply Greater_imp_ap. auto. apply pos_div_two. astepl ([0][+]ZeroR). apply plus_resp_less_leEq. apply pos_one. auto. Qed.
imports: CoRN.reals.Max_AbsIR CoRN.algebra.Expon CoRN.algebra.CPoly_ApZero