let n be Nat; ((n |^ 2) + (3 * n)) + 2 = (n + 1) * (n + 2)
(n + 1) * (n + 2) =
((n * n) + ((2 * n) + (1 * n))) + 2
.=
(((n |^ 1) * n) + ((2 + 1) * n)) + 2
.=
((n |^ (1 + 1)) + ((2 + 1) * n)) + 2
by NEWTON:6
;
hence
((n |^ 2) + (3 * n)) + 2 = (n + 1) * (n + 2)
; verum