define int_summation : (fn (UInt, UInt, (fn UInt -> Int)) -> Int) = fun k:UInt, begin:UInt, f:(fn UInt -> Int) {
      int_summation_nat(toNat(k), toNat(begin), f)
    }

int_summation_add: (all a:UInt. (all b:UInt, s:UInt, t:UInt, f:(fn UInt -> Int), g:(fn UInt -> Int), h:(fn UInt -> Int). (if ((all i:Nat. (if i < toNat(a) then g(s + fromNat(i)) = f(s + fromNat(i)))) and (all i:Nat. (if i < toNat(b) then h(t + fromNat(i)) = f((s + a) + fromNat(i))))) then int_summation(a + b, s, f) = int_summation(a, s, g) + int_summation(b, t, h))))

int_summation_add_pointwise: (all k:UInt, s:UInt, f:(fn UInt -> Int), g:(fn UInt -> Int). int_summation(k, s, fun i:UInt { f(i) + g(i) }) = int_summation(k, s, f) + int_summation(k, s, g))

int_summation_cong: (all k:UInt. (all f:(fn UInt -> Int), g:(fn UInt -> Int), s:UInt, t:UInt. (if (all i:Nat. (if i < toNat(k) then f(s + fromNat(i)) = g(t + fromNat(i)))) then int_summation(k, s, f) = int_summation(k, t, g))))

int_summation_const_zero: (all k:UInt, s:UInt. int_summation(k, s, fun i:UInt { +0 }) = +0)

recursive int_summation_nat(Nat,Nat,(fn UInt -> Int)) -> Int{
  int_summation_nat(zero, begin, f) = +0
  int_summation_nat(suc(k), begin, f) = f(fromNat(begin)) + int_summation_nat(k, suc(begin), f)
}

int_summation_neg: (all k:UInt, s:UInt, f:(fn UInt -> Int). int_summation(k, s, fun i:UInt { - f(i) }) = - int_summation(k, s, f))

int_summation_next: (all n:UInt, s:UInt, f:(fn UInt -> Int). int_summation(1 + n, s, f) = int_summation(n, s, f) + f(s + n))

int_summation_sub: (all k:UInt, s:UInt, f:(fn UInt -> Int), g:(fn UInt -> Int). int_summation(k, s, fun i:UInt { f(i) - g(i) }) = int_summation(k, s, f) - int_summation(k, s, g))

int_summation_zero: (all begin:UInt, f:(fn UInt -> Int). int_summation(0, begin, f) = +0)