proposition: Lemma sum_reciprocal_triangular : Rser_cv (fun n => / triangle (S n)) 2.
proof: Proof. replace 2 with (2 * 1) by (compute; field). apply Rseq_cv_eq_compat with (Rseq_mult (Rseq_constant 2) (sum_f_R0 inv_snssn)). intro n. unfold Rseq_mult, Rseq_inv, Rseq_constant, inv_snssn, triangle. rewrite scal_sum. apply Rseq_sum_ext; intro. elim_ident. field. INR_solve. apply Rseq_cv_mult_compat. auto with *. apply ser_cv_inv_snssn. Qed.
imports: Reals Rseries_RiemannInt Rseries_facts Rtactic Rsequence_facts Lra