proposition: Lemma derive_pt_recip_interv_prelim0 (f g:R->R) (lb ub x:R) (Prf:derivable_pt f (g x)) (Prg:derivable_pt g x) : lb < ub -> lb < x < ub -> (forall x, lb < x < ub -> (comp f g) x = id x) -> derive_pt f (g x) Prf <> 0 -> derive_pt g x Prg = 1 / (derive_pt f (g x) Prf).
proof: Proof. intros lb_lt_ub x_encad local_recip Df_neq. replace (derive_pt g x Prg) with ((derive_pt g x Prg) * (derive_pt f (g x) Prf) * / (derive_pt f (g x) Prf)). { unfold Rdiv. rewrite (Rmult_comm _ (/ derive_pt f (g x) Prf)). rewrite (Rmult_comm _ (/ derive_pt f (g x) Prf)). apply Rmult_eq_compat_l. rewrite Rmult_comm. rewrite <- derive_pt_comp. assert (x_encad2 : lb <= x <= ub) by intuition. rewrite pr_nu_var2_interv with (g:=id) (pr2:= derivable_pt_id_interv lb ub x x_encad2) (lb:=lb) (ub:=ub) ; [reg| | |] ; assumption. } rewrite Rmult_assoc, Rinv_r. { intuition. } assumption. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra