proposition: Lemma derivable_pt_recip_interv_prelim0 : forall (f g : R -> R) (lb ub x : R) (Prf : forall a : R, g lb <= a <= g ub -> derivable_pt f a), continuity_pt g x -> lb < ub -> lb < x < ub -> forall Prg_incr : g lb <= g x <= g ub, (forall x0 : R, lb <= x0 <= ub -> comp f g x0 = id x0) -> derive_pt f (g x) (Prf (g x) Prg_incr) <> 0 -> derivable_pt g x.
proof: Proof. intros f g lb ub x Prf g_cont_pt lb_lt_ub x_encad Prg_incr f_eq_g Df_neq. unfold derivable_pt, derivable_pt_abs. exists (1 / derive_pt f (g x) (Prf (g x) Prg_incr)). apply derivable_pt_lim_recip_interv ; assumption. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra