proposition: Lemma derivable_pt_recip_interv_prelim1_decr : forall (f g:R->R) (lb ub x : R), lb < ub -> f ub < x < f lb -> (forall x : R, f ub <= x -> x <= f lb -> lb <= g x <= ub) -> (forall a : R, lb <= a <= ub -> derivable_pt f a) -> derivable_pt f (g x).
proof: Proof. intros f g lb ub x lb_lt_ub x_encad g_wf f_deriv. apply f_deriv. apply g_wf; lra. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra