proposition: Lemma sum_consecutive_triangle n : triangle (S n) + triangle n = INR (S n) * INR (S n).
proof: Proof. intros. unfold triangle. elim_ident. field. Qed.
imports: Reals Rseries_RiemannInt Rseries_facts Rtactic Rsequence_facts Lra