proposition: Lemma reciprocal_opp_compat_interval : forall f g lb ub, reciprocal_interval lb ub f g -> reciprocal_interval lb ub (fun x =>f(-x)) (-g)%F.
proof: Proof. intros f g lb ub f_recip_g x x_in_I. unfold comp, opp_fct ; simpl ; rewrite Ropp_involutive ; apply f_recip_g ; assumption. 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