import Nat

sum_n: (all n:Nat. ℕ2 * summation(n, ℕ0, fun x { x }) = n * (n ∸ ℕ1))

sum_n': (all n:Nat. ℕ2 * summation(suc(n), ℕ0, fun x { x }) = n * (n + ℕ1))