proposition: Lemma continuity_open_interval_Ropp_compat : forall f lb ub, continuity_open_interval lb ub f -> continuity_open_interval (- ub) (- lb) (fun x => f (- x)).
proof: Proof. intros f lb ub Hf b b_in eps eps_pos. assert (mb_in : open_interval lb ub (- b)). destruct b_in ; split ; lra. destruct (Hf _ mb_in _ eps_pos) as [alpha [alpha_pos Halpha]] ; exists alpha ; split ; [assumption | intros x [x_in x_bd]]. apply Halpha ; split ; simpl. destruct x_in ; split ; lra. rewrite R_dist_opp_compat ; assumption. Qed.
imports: Rbase Ranalysis Rinterval Rfunctions Rfunction_def Ranalysis_def Ranalysis_def_simpl Rfunction_facts MyRIneq MyR_dist Lra Tactics