proposition: Lemma Rint_inv : forall a b, 0 < a <= b -> Rint (fun x => /x) a b (ln b - ln a).
proof: Proof. intros a b Hab. apply Rint_derive. intuition. intros x Hx. apply derivable_pt_lim_ln. apply Rlt_le_trans with a; intuition. intros x Hx. apply continuity_pt_inv. apply derivable_continuous, derivable_id. assert( 0 < x). apply Rlt_le_trans with a; tauto. auto with *. Qed.
imports: Reals MyRfunctions Rintegral Lia