reconsider x = (b - 1) / 2 as Nat ;
reconsider k = a |^ (2 * x) as square Nat ;
a |^ ((2 * x) + 1) = (a |^ (2 * x)) * a by NEWTON:6;
hence not a |^ b is square ; :: thesis: verum