The triangular numbers

module elementary-number-theory.triangular-numbers where

Imports

open import elementary-number-theory.addition-natural-numbers
open import elementary-number-theory.natural-numbers

Definition

triangular-number-ℕ : ℕ → ℕ
triangular-number-ℕ 0 = 0
triangular-number-ℕ (succ-ℕ n) = (triangular-number-ℕ n) +ℕ (succ-ℕ n)