We want to prove

.N:Nat (squsum(N) * 6 = (N * N * N * 2) + (N * N * 3) + N)

- Base case : prove assertion for
N = 0 - Show
squsum(0) * 6 = (0 * 0 * 0 * 2) + (0 * 0 * 3) + 0

- Show
- Induction case : prove assertion for
N = s M N = M - Quantifier elimination introduces new
constant *m :Nat*. - Implication elimination assumes
squsum(m) * 6 = (m * m * m * 2) + (m * m * 3) + m - Change hypothesis
squsum(m) * 6 = (m * m * m * 2) + (m * m * 3) + m - Show
squsum(s m) * 6 = (s m * s m * s m * 2) + (s m * s m * 3) + s m

- Quantifier elimination introduces new