proposition: Lemma difference_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