real_diff_squares: (all a:Real, b:Real. a * a - b * b = (a - b) * (a + b))

real_sqrt_abs_square: (all x:Real. sqrt(x * x) = abs(x))

real_sqrt_le_mono: (all x:Real, y:Real. (if ((real(+0) ≤ x) and (x ≤ y)) then sqrt(x) ≤ sqrt(y)))

real_sqrt_mult: (all x:Real, y:Real. (if ((real(+0) ≤ x) and (real(+0) ≤ y)) then sqrt(x * y) = sqrt(x) * sqrt(y)))

real_sqrt_nonneg: (all x:Real. (if real(+0) ≤ x then real(+0) ≤ sqrt(x)))

real_sqrt_of_square: (all y:Real. (if real(+0) ≤ y then sqrt(y * y) = y))

real_sqrt_one: sqrt(real(+1)) = real(+1)

real_sqrt_square: (all x:Real. (if real(+0) ≤ x then sqrt(x) * sqrt(x) = x))

real_sqrt_unique: (all x:Real, y:Real. (if ((real(+0) ≤ y) and (y * y = x)) then sqrt(x) = y))

real_sqrt_zero: sqrt(real(+0)) = real(+0)

real_square_injective: (all a:Real, b:Real. (if ((real(+0) ≤ a) and (real(+0) ≤ b) and (a * a = b * b)) then a = b))

real_square_less: (all a:Real, b:Real. (if ((real(+0) ≤ a) and (a < b)) then a * a < b * b))