proposition: Lemma derive_pt_recip_interv_prelim1_0 : 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:= f_incr_implies_g_incr_interv f g lb ub lb_lt_ub f_incr f_eq_g g_wf). assert (Left_inv := leftinv_is_rightinv_interv f g lb ub f_incr f_eq_g g_wf). unfold comp, id in Left_inv. split ; [rewrite <- Left_inv with (x:=lb) | rewrite <- Left_inv ];intuition. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra