proposition: Lemma reciprocal_opp_compat_interval2 : forall f g lb ub, reciprocal_interval lb ub f g -> reciprocal_interval (-ub) (-lb) (-f)%F (fun x => g (-x)).
proof: Proof. intros f g lb ub f_recip_g x x_in_I. unfold opp_fct ; rewrite f_recip_g. apply Ropp_involutive. unfold interval in * ; destruct x_in_I ; split ; lra. Qed.
imports: Rbase Rpower Ranalysis Lra Rfunctions Rfunction_def Rextensionality MyRIneq MyR_dist Rtopology Rinterval Ranalysis_def Ranalysis_def_simpl Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity