proposition: Lemma f_incr_implies_g_incr_interv : forall f g:R->R, forall lb ub, lb < ub -> (forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) -> (forall x, f lb <= x -> x <= f ub -> (comp f g) x = id x) -> (forall x , f lb <= x -> x <= f ub -> lb <= g x <= ub) -> (forall x y, f lb <= x -> x < y -> y <= f ub -> g x < g y).
proof: Proof. intros f g lb ub lb_lt_ub f_incr f_eq_g g_ok x y lb_le_x x_lt_y y_le_ub. assert (x_encad : f lb <= x <= f ub) by lra. assert (y_encad : f lb <= y <= f ub) by lra. assert (gx_encad := g_ok _ (proj1 x_encad) (proj2 x_encad)). assert (gy_encad := g_ok _ (proj1 y_encad) (proj2 y_encad)). case (Rlt_dec (g x) (g y)); [ easy |]. intros Hfalse. assert (Temp := Rnot_lt_le _ _ Hfalse). enough (y <= x) by lra. replace y with (id y) by easy. replace x with (id x) by easy. rewrite <- f_eq_g by easy. rewrite <- f_eq_g by easy. assert (f_incr2 : forall x y, lb <= x -> x <= y -> y < ub -> f x <= f y). { intros m n lb_le_m m_le_n n_lt_ub. case (m_le_n). - intros; apply Rlt_le, f_incr, Rlt_le; assumption. - intros Hyp; rewrite Hyp; apply Req_le; reflexivity. } apply f_incr2; intuition. enough (g x <> ub) by lra. intro Hf. assert (Htemp : (comp f g) x = f ub). { unfold comp; rewrite Hf; reflexivity. } rewrite f_eq_g in Htemp by easy. unfold id in Htemp. lra. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra