proposition: Lemma derive_pt_recip_interv_prelim1_1 : forall (f g:R->R) (lb ub x:R), lb < ub -> f lb < x < f ub -> (forall x y : R, lb <= x -> x < y -> y <= ub -> f x < f y) -> (forall x : R, f lb <= x -> x <= f ub -> lb <= g x <= ub) -> (forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) -> lb <= g x <= ub.
proof: Proof. intros f g lb ub x lb_lt_ub x_encad f_incr g_wf f_eq_g. assert (Temp := derive_pt_recip_interv_prelim1_0 f g lb ub x lb_lt_ub x_encad f_incr g_wf f_eq_g). split ; apply Rlt_le ; intuition. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra