proposition: Theorem continuity_pt_gt : forall f x y, (y < f x)%R -> continuity_pt f x -> locally_true x (fun u => (y < f u)%R).
proof: Proof. intros. generalize (Ropp_lt_contravar _ _ H). clear H. intro H. generalize (continuity_pt_opp _ _ H0). clear H0. intro H0. destruct (continuity_pt_lt (opp_fct f) _ _ H H0) as (delta, (Hdelta, H1)). exists delta. split. exact Hdelta. intros. apply Ropp_lt_cancel. exact (H1 _ H2). Qed.
imports: Coq(ZArith Reals Psatz) Flocq(Raux)