proposition: Lemma sum_triangular_tetrahedral n : sum_f_R0 triangle n = INR (n * S n * S (S n)) / 6.
proof: Proof. unfold triangle. induction n. simpl. field. rewrite tech5, IHn. elim_ident. field. Qed.
imports: Reals Rseries_RiemannInt Rseries_facts Rtactic Rsequence_facts Lra