proposition: Lemma eps_exists_1 : forall eps x y : IR, [0] [<] eps -> [0] [<] x -> [0] [<] y -> {eps' : IR | [0] [<] eps' | eps' [<=] eps /\ x[*]eps' [<=] y}.
proof: Proof. intros eps x y Heps Hx Hy. cut ([0] [<] Half[*]eps). intro H2. cut (x [#] [0]). intro H3. 2: apply pos_ap_zero; auto. elim (less_cotransitive_unfolded _ _ _ H2 ((y[/] x[//]H3) [-]Half[*]eps)); intro H5. exists (Half[*]eps). auto. split. apply less_leEq; apply half_3. auto. astepr (x[*] (y[/] x[//]H3)). apply less_leEq. apply mult_resp_less_lft; auto. astepl ([0][+]Half[*]eps). apply shift_plus_less; auto. cut ([0] [<] (y[/] x[//]H3)). intro H4. 2: apply div_resp_pos; auto. exists (Half[*] (y[/] x[//]H3)). apply mult_resp_pos. apply pos_half. auto. split. apply leEq_transitive with (y[/] x[//]H3). apply less_leEq; apply half_3; auto. apply less_leEq. astepr ([1][*]eps). astepr ((Half[+]Half) [*]eps). astepr (Half[*]eps[+]Half[*]eps). apply shift_less_plus'; auto. rstepl (Half[*]y). apply less_leEq; apply half_3; auto. apply mult_resp_pos; auto. apply pos_half. Qed.
imports: CoRN.complex.NRootCC CoRN.complex.AbsCC CoRN.fta.MainLemma