proposition: Lemma Rint_inv1 : forall a b, -1 < a <= b -> Rint (/(id + fct_cte 1))%F a b (ln (b + 1) - ln (a + 1)).
proof: Proof. intros a b Hab. replace (ln (b + 1)) with (comp ln (id + fct_cte 1) b) by reflexivity. replace (ln (a + 1)) with (comp ln (id + fct_cte 1) a) by reflexivity. apply Rint_derive. intuition. intros x Hx. replace ((/ (id + fct_cte 1))%F x) with ((/ (id + fct_cte 1))%F x * (1+0)) by ring. apply derivable_pt_lim_comp. apply derivable_pt_lim_plus. apply derivable_pt_lim_id. apply derivable_pt_lim_const. apply derivable_pt_lim_ln. unfold plus_fct, fct_cte, id. intuition. apply Rlt_le_trans with (a + 1); lra. intros x Hx. apply continuity_pt_inv. apply continuity_pt_plus. apply derivable_continuous, derivable_id. apply continuity_pt_const. unfold fct_cte; intros u v; reflexivity. unfold fct_cte, id, plus_fct. assert(0 < x + 1). apply Rlt_le_trans with (a + 1). replace 0 with (- 1 + 1) by ring. apply Rplus_lt_compat_r; intuition. apply Rplus_le_compat_r; intuition. auto with *. Qed.
imports: Reals Rseries_def Rseries_facts RiemannInt Lra Rsequence_facts Rsequence_subsequence Riemann_integrable Rintegral