proposition: Lemma derive_pt_recip_interv_prelim0 : forall (f g:R->R) (lb ub x:R) (Prf:derivable_pt f (g x)) (Prg:derivable_pt g x), open_interval lb ub x -> reciprocal_open_interval lb ub f g -> derive_pt f (g x) Prf <> 0 -> derive_pt g x Prg = 1 / (derive_pt f (g x) Prf).
proof: Proof. intros f g lb ub x Df Dg x_in_I local_recip Df_neq. replace (derive_pt g x Dg) with ((derive_pt g x Dg) * (derive_pt f (g x) Df) * / (derive_pt f (g x) Df)) by (field ; assumption). unfold Rdiv ; apply Rmult_eq_compat_r. rewrite Rmult_comm, <- derive_pt_comp. erewrite pr_nu_var2_interv. eapply derive_pt_id. eassumption. auto. 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