proposition: Lemma derive_pt_recip_interv_prelim1_1 : forall f g lb ub x, lb <= ub -> open_interval (f lb) (f ub) x -> strictly_increasing_interval lb ub f -> (forall x : R, interval (f lb) (f ub) x -> interval lb ub (g x)) -> reciprocal_interval (f lb) (f ub) f g -> interval lb ub (g x).
proof: Proof. intros ; eapply open_interval_interval, derive_pt_recip_interv_prelim1_0 ; eassumption. Qed.
imports: Rbase Ranalysis Rfunctions Rfunction_def Rseries_def Lra RiemannInt SeqProp PeanoNat RIneq MyRIneq Ranalysis_def Ranalysis_def_simpl Ranalysis_facts Ranalysis_continuity Ranalysis_derivability Ranalysis_monotonicity Rinterval RIVT