proposition: Lemma continuity_pt_in_opp_rev : forall f D x, continuity_pt_in D (- f)%F x -> continuity_pt_in D f x.
proof: Proof. intros f D x Hf x_in ; apply limit1_in_ext with (- - f)%F. intros y y_in ; apply Ropp_involutive. rewrite <- (Ropp_involutive (f x)) ; apply limit_Ropp, Hf ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Ranalysis_def_simpl Rfunction_facts MyRIneq MyR_dist Lra Tactics