proposition: Lemma continuity_interval_Ropp_compat_rev : forall f lb ub, continuity_interval (- ub) (- lb) (fun x => f (- x)) -> continuity_interval lb ub f.
proof: Proof. intros f lb ub Hf ; pose (F := fun x => f (- x)) ; apply continuity_in_ext with (fun x => F (- x)). intro x ; unfold F ; f_equal ; apply Ropp_involutive. rewrite <- (Ropp_involutive lb), <- (Ropp_involutive ub) ; apply continuity_interval_Ropp_compat, Hf. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Ranalysis_def_simpl Rfunction_facts MyRIneq MyR_dist Lra Tactics