proposition: Lemma leftinv_is_rightinv_interv : forall (f g:R->R) (lb ub:R), (forall x y, lb <= x -> x < y -> y <= ub -> f x < f y) -> (forall y, f lb <= y -> y <= f ub -> (comp f g) y = id y) -> (forall x, f lb <= x -> x <= f ub -> lb <= g x <= ub) -> forall x, lb <= x <= ub -> (comp g f) x = id x.
proof: Proof. intros f g lb ub f_incr_interv Hyp g_wf x x_encad. assert(f_inj : forall x y, lb <= x <= ub -> lb <= y <= ub -> f x = f y -> x = y). { intros a b a_encad b_encad fa_eq_fb. case(total_order_T a b). { intro s ; case s ; clear s. { intro Hf. assert (Hfalse := f_incr_interv a b (proj1 a_encad) Hf (proj2 b_encad)). apply False_ind. apply (Rlt_not_eq (f a) (f b)) ; assumption. } intuition. } intro Hf. assert (Hfalse := f_incr_interv b a (proj1 b_encad) Hf (proj2 a_encad)). apply False_ind. apply (Rlt_not_eq (f b) (f a)) ; [|symmetry] ; assumption. } assert (f_incr_interv2 : forall x y, lb <= x -> x <= y -> y <= ub -> f x <= f y). { intros m n cond1 cond2 cond3. case cond2. { intro cond. apply Rlt_le ; apply f_incr_interv ; assumption. } intro cond ; right ; rewrite cond ; reflexivity. } assert (Hyp2:forall x, lb <= x <= ub -> f (g (f x)) = f x). { intros ; apply Hyp. { apply f_incr_interv2 ; intuition. } apply f_incr_interv2 ; intuition. } unfold comp ; unfold comp in Hyp. apply f_inj. { apply g_wf ; apply f_incr_interv2 ; intuition. } { unfold id ; assumption. } apply Hyp2 ; unfold id ; assumption. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra