proposition: Lemma eps_exists : forall eta a_0 : IR, [0] [<] eta -> [0] [<] a_0 -> {eps : IR | [0] [<] eps | Two[*] (Three[^]n[+][1]) [*]eps [<=] eta /\ Three[*]eps [<=] Smaller[*]a_0 /\ eps [<=] a_0}.
proof: Proof. intros eta a_0 Heta Ha_0. elim (eps_exists_1 ((Smaller[*]a_0) [/]ThreeNZ) (Three[^]n[+][1]) (eta [/]TwoNZ)). intros eps H H0. elim H0; intros H1 H2. exists eps. auto. split. astepl (Two[*] ((Three[^]n[+][1]) [*]eps)). apply shift_mult_leEq' with (two_ap_zero IR); auto. apply pos_two. split. apply shift_mult_leEq' with (three_ap_zero IR); auto. apply pos_three. eapply leEq_transitive. apply H1. apply shift_div_leEq'. apply pos_three. apply mult_resp_leEq_rht. unfold Smaller in |- *; apply leEq_transitive with OneR. apply p3m_small. apply less_leEq; apply one_less_three. apply less_leEq; auto. apply pos_div_three. apply mult_resp_pos; auto. unfold Smaller in |- *; apply p3m_pos. apply plus_resp_pos. apply nexp_resp_pos. apply pos_three. apply pos_one. apply pos_div_two; auto. Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma