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))