Description: The square of a real is nonnegative, deduction form. (Contributed by Mario Carneiro, 28-May-2016)