proposition: Lemma f_contin_pos : forall z : IR, [0] [<] f z -> {eps : IR | [0] [<] eps | forall x, x [<=] z[+]eps -> z [<=] x[+]eps -> [0] [<] f x}.
proof: Proof. intros z H. unfold contin in f_contin. unfold continAt in f_contin. unfold funLim in f_contin. unfold AbsSmall in f_contin. elim (f_contin z (f z [/]TwoNZ) (pos_div_two _ _ H)). intro eps. intros H1 H2. exists eps. auto. intros. elim (H2 x). intros H5 H6. astepl (f z[-]f z). apply shift_minus_less. apply shift_less_plus'. apply leEq_less_trans with (f z [/]TwoNZ). auto. apply pos_div_two'. auto. split. apply shift_leEq_minus. rstepl (x[-]eps). apply shift_minus_leEq. auto. apply shift_minus_leEq. astepr (x[+]eps). auto. Qed.
imports: CoRN.reals.CPoly_Contin