proposition: Theorem continuity_pt_lt : forall f x y, (f x < y)%R -> continuity_pt f x -> locally_true x (fun u => (f u < y)%R).
proof: Proof. intros. assert (0 < y - f x)%R. apply Rplus_lt_reg_l with (f x). rewrite Rplus_0_r. replace (f x + (y - f x))%R with y. 2: ring. exact H. destruct (H0 _ H1) as (delta, (Hdelta, H2)). clear H0. exists delta. split. exact Hdelta. intros. case (Req_dec h 0) ; intro H3. rewrite H3. rewrite Rplus_0_r. exact H. generalize (H2 (x + h)%R). clear H2. unfold R_met, R_dist, D_x, no_cond. simpl. intro. apply Rplus_lt_reg_r with (- f x)%R. apply Rle_lt_trans with (1 := RRle_abs (f (x + h) - f x)%R). apply H2. assert (x + h - x = h)%R. ring. split. split. exact I. intro H5. elim H3. rewrite <- H4. rewrite <- H5. exact (Rplus_opp_r _). rewrite H4. exact H0. Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)