prelude_aux: THEORY BEGIN x: VAR real y: VAR nonzero_real n: VAR nat abs_div : LEMMA abs(x / y) = abs(x) / abs(y) abs_abs : LEMMA abs(abs(x)) = abs(x) abs_square : LEMMA abs(x * x) = x * x abs_hat_nat : LEMMA abs(x)^n = abs(x^n) even_plus1 : LEMMA even?(n) IFF NOT even?(n+1) even_int : LEMMA even?(n) IMPLIES integer_pred((n / 2)) not_even_int: LEMMA NOT even?(n) IMPLIES integer_pred(((n - 1) / 2)) sq_lt_1 : LEMMA x*x < 1 IMPLIES abs(x) < 1 sq_le_1 : LEMMA x*x <= 1 IMPLIES abs(x) <= 1 % sqrt_1_gt : LEMMA x*x > 1 IMPLIES abs(x) > 1 % sqrt_1_ge : LEMMA x*x <= 1 IMPLIES abs(x) <= 1 END prelude_aux