proposition: Lemma triangle_sum n : sum_f_R0 INR n = triangle n.
proof: Proof. unfold triangle. induction n. simpl; field. rewrite tech5. rewrite IHn. elim_ident. field. Qed.
imports: Reals Rseries_RiemannInt Rseries_facts Rtactic Rsequence_facts Lra