let s be non trivial Nat; :: thesis: for x being s -gonal number holds 0 <= (((8 * s) - 16) * x) + ((s - 4) ^2)
let x be s -gonal number ; :: thesis: 0 <= (((8 * s) - 16) * x) + ((s - 4) ^2)
s - 2 >= 2 - 2 by XREAL_1:9, NAT_2:29;
then 8 * (s - 2) >= 0 ;
hence 0 <= (((8 * s) - 16) * x) + ((s - 4) ^2) ; :: thesis: verum