proposition: Lemma f_contin_neg : forall z : IR, f z [<] [0] -> {eps : IR | [0] [<] eps | forall x, x [<=] z[+]eps -> z [<=] x[+]eps -> f x [<] [0]}.
proof: Proof. intros. unfold contin in f_contin. unfold continAt in f_contin. unfold funLim in f_contin. unfold AbsSmall in f_contin. cut ([0] [<] [--] (f z)). intro H0. elim (f_contin z ( [--] (f z) [/]TwoNZ) (pos_div_two _ _ H0)). intro eps. intros H2 H3. exists eps. auto. intros. elim (H3 x). intros H6 H7. rstepr (f z[-][--][--] (f z)). apply shift_less_minus'. apply shift_plus_less. apply less_leEq_trans with (f z [/]TwoNZ). astepl (f z). apply inv_cancel_less. rstepl ( [--] (f z) [/]TwoNZ). apply pos_div_two'. auto. rstepl ( [--] ( [--] (f z) [/]TwoNZ)). auto. split. apply shift_leEq_minus. rstepl (x[-]eps). apply shift_minus_leEq. auto. apply shift_minus_leEq. astepr (x[+]eps). auto. astepl ( [--]ZeroR). apply inv_resp_less. auto. Qed.
imports: CoRN.reals.CPoly_Contin