proposition: Lemma leftinv_is_rightinv : forall (f g:R->R), (forall x y, x < y -> f x < f y) -> (forall x, (comp f g) x = id x) -> (forall x, (comp g f) x = id x).
proof: Proof. intros f g f_incr Hyp x. assert(f_inj : forall x y, f x = f y -> x = y). { intros a b fa_eq_fb. pose proof (f_incr a b);pose proof (f_incr b a);lra. } apply f_inj,Hyp. Qed.
imports: Rbase Ranalysis_reg Rfunctions Rseries RiemannInt SeqProp Lia Lra