proposition: Lemma RinvN_pos : forall n:nat, 0 < / (INR n + 1).
proof: Proof. intro; apply Rinv_0_lt_compat; apply Rplus_le_lt_0_compat; [ apply pos_INR | apply Rlt_0_1 ]. Qed.
imports: Rfunctions SeqSeries Ranalysis_reg Rbase RiemannInt_SF RList Lra