Nuprl - mb_nat LEMMAs for sum

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

Theorem	Name
Thm* n:, f,g:(n), d:. Thm* sum(f(x)-g(x) \| x < n) = d sum(f(x) \| x < n) = sum(g(x) \| x < n)+d	[sum_difference]
cites the following:
Thm* n:, f,g:(n). Thm* sum(f(x) \| x < n)+sum(g(x) \| x < n) = sum(f(x)+g(x) \| x < n)	[sum_linear]
Thm* n:, f,g:(n). Thm* (i:n. f(i) = g(i)) sum(f(x) \| x < n) = sum(g(x) \| x < n)	[sum_functionality]

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html