proposition: Lemma derivable_pt_in_reciprocal_interval_rev: forall f g lb ub, (forall x : R, interval (f lb) (f ub) x -> interval lb ub (g x)) -> forall x, interval (f lb) (f ub) x -> derivable_interval lb ub f -> derivable_pt_in (interval lb ub) f (g x).
proof: Proof. intros f g lb ub g_ok x x_in Df ; apply Df, g_ok ; assumption. 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