8. Gauss’s sum
sumTo n adds up the numbers from 0 to n. Prove Gauss’s formula in a form without division: 2 * sumTo n = n * (n + 1).
omega handles linear arithmetic, but it treats a product of two variables as an opaque value. Expand the products first so both sides contain the same ones.
Running and submitting solutions, the hints and the editorial come with the Academy Pass. The daily problem is open to every account.
1def sumTo : Nat → Nat
2 | 0 => 0
3 | n + 1 => (n + 1) + sumTo n
4theorem solution (n : Nat) : 2 * sumTo n = n * (n + 1) := by
givenLoading editor…
Type
\to in the editor, or click:Where you start. Everything above ⊢ may be assumed; the line below it is what you must prove.
n:Nat
⊢2 * sumTo n = n * (n + 1)
ReadyLn 1, Col 1Lean 4
Draft saved in this browser