is mentioned by

Thm* n:, a,b:. sum(a+bi | i < n) = ((n(a+a+b(n-1))) 2)	[sum_arith]
Thm* n:, a,b:. sum(a+bi | i < n)2 = n(a+a+b(n-1))	[sum_arith1]
Thm* k:, f,g:(k), p:(k). sum(if p(i) f(i)+g(i) else f(i) fi | i < k) = sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k)	[sum-ite]
Thm* k,b:, f:(k). (x:k. bf(x)) bksum(f(x) | x < k)	[sum_lower_bound]
Thm* k,b:, f:(k). (x:k. f(x)b) sum(f(x) | x < k)bk	[sum_bound]
Thm* k:, f,g:(k). (x:k. f(x)g(x)) sum(f(x) | x < k)sum(g(x) | x < k)	[sum_le]

In prior sections: mb nat mb list 2

Try larger context: Graphs