let n be Nat; (((n * (4 * (n |^ 2))) + (11 * n)) + (12 * (n |^ 2))) + 3 = (n + 1) * ((4 * ((n + 1) |^ 2)) - 1)
(n + 1) * ((4 * ((n + 1) |^ 2)) - 1) =
(n + 1) * ((4 * (((n |^ 2) + ((2 * n) * 1)) + (1 |^ 2))) - 1)
by Lm3
.=
(n + 1) * ((4 * (((n |^ 2) + (2 * n)) + 1)) - 1)
.=
(((n * (4 * (n |^ 2))) + (4 * (n |^ 2))) + ((8 * (n * n)) + (8 * n))) + ((3 * n) + (3 * 1))
.=
(((n * (4 * (n |^ 2))) + (4 * (n |^ 2))) + ((8 * (n |^ 2)) + (8 * n))) + ((3 * n) + (3 * 1))
by WSIERP_1:1
.=
(((n * (4 * (n |^ 2))) + ((4 * (n |^ 2)) + (8 * (n |^ 2)))) + ((8 * n) + (3 * n))) + 3
;
hence
(((n * (4 * (n |^ 2))) + (11 * n)) + (12 * (n |^ 2))) + 3 = (n + 1) * ((4 * ((n + 1) |^ 2)) - 1)
; verum