proposition: Lemma derivable_pt_in_reciprocal_interval : forall f g lb ub, reciprocal_interval lb ub f g -> forall x Df_gx, open_interval (g lb) (g ub) (g x) -> continuity_pt_in (open_interval lb ub) g x -> open_interval lb ub x -> derive_pt_in (interval (g lb) (g ub)) f (g x) Df_gx <> 0 -> derivable_pt_in (open_interval lb ub) g x.
proof: Proof. intros ; eexists ; eapply derivable_pt_lim_in_reciprocal_interval ; 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