They do do the proofs that way!
|------
(FORALL (n: nat):
sum(n, square) = (n * (n + 1) * (2 * n + 1)) / 6)
Rerunning step: (INDUCT-AND-SIMPLIFY “n”)
square rewrites square(0)
to 0
sum rewrites sum(0, square)
to 0
square rewrites square(1+j!1)
to 1+j!1+(j!1*j!1+j!1)
sum rewrites sum(1+j!1, square)
to 1+sum(j!1, square)+j!1*j!1+j!1+j!1
By induction on n, and by repeatedly rewriting and simplifying,
Q.E.D.