(* ========================================================================= *)
(* More basic properties of the reals.                                       *)
(*                                                                           *)
(*       John Harrison, University of Cambridge Computer Laboratory          *)
(*                                                                           *)
(*            (c) Copyright, University of Cambridge 1998                    *)
(*              (c) Copyright, John Harrison 1998-2007                       *)
(*              (c) Copyright, Valentina Bruno 2010                          *)
(* ========================================================================= *)

needs "realarith.ml";;

(* ------------------------------------------------------------------------- *)
(* Additional commutativity properties of the inclusion map.                 *)
(* ------------------------------------------------------------------------- *)

let REAL_OF_NUM_LT = 
prove (`!m n. &m < &n <=> m < n`,
REWRITE_TAC[real_lt; GSYM NOT_LE; REAL_OF_NUM_LE]);;
let REAL_OF_NUM_GE = 
prove (`!m n. &m >= &n <=> m >= n`,
REWRITE_TAC[GE; real_ge; REAL_OF_NUM_LE]);;
let REAL_OF_NUM_GT = 
prove (`!m n. &m > &n <=> m > n`,
REWRITE_TAC[GT; real_gt; REAL_OF_NUM_LT]);;
let REAL_OF_NUM_MAX = 
prove (`!m n. max (&m) (&n) = &(MAX m n)`,
REWRITE_TAC[REAL_OF_NUM_LE; MAX; real_max; GSYM COND_RAND]);;
let REAL_OF_NUM_MIN = 
prove (`!m n. min (&m) (&n) = &(MIN m n)`,
REWRITE_TAC[REAL_OF_NUM_LE; MIN; real_min; GSYM COND_RAND]);;
let REAL_OF_NUM_SUC = 
prove (`!n. &n + &1 = &(SUC n)`,
REWRITE_TAC[ADD1; REAL_OF_NUM_ADD]);;
let REAL_OF_NUM_SUB = 
prove (`!m n. m <= n ==> (&n - &m = &(n - m))`,
REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN STRIP_TAC THEN ASM_REWRITE_TAC[ADD_SUB2] THEN REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN ONCE_REWRITE_TAC[REAL_ADD_SYM] THEN REWRITE_TAC[real_sub; GSYM REAL_ADD_ASSOC] THEN MESON_TAC[REAL_ADD_LINV; REAL_ADD_SYM; REAL_ADD_LID]);;
(* ------------------------------------------------------------------------- *) (* A few theorems we need to prove explicitly for later. *) (* ------------------------------------------------------------------------- *)
let REAL_MUL_AC = 
prove (`(m * n = n * m) /\ ((m * n) * p = m * (n * p)) /\ (m * (n * p) = n * (m * p))`,
REWRITE_TAC[REAL_MUL_ASSOC; EQT_INTRO(SPEC_ALL REAL_MUL_SYM)] THEN AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_ACCEPT_TAC REAL_MUL_SYM);;
let REAL_ADD_RDISTRIB = 
prove (`!x y z. (x + y) * z = x * z + y * z`,
MESON_TAC[REAL_MUL_SYM; REAL_ADD_LDISTRIB]);;
let REAL_LT_LADD_IMP = 
prove (`!x y z. y < z ==> x + y < x + z`,
REPEAT GEN_TAC THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[real_lt] THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LE_LADD_IMP) THEN DISCH_THEN(MP_TAC o SPEC `--x`) THEN REWRITE_TAC[REAL_ADD_ASSOC; REAL_ADD_LINV; REAL_ADD_LID]);;
let REAL_LT_MUL = 
prove (`!x y. &0 < x /\ &0 < y ==> &0 < x * y`,
REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LT_LE] THEN CONV_TAC(ONCE_DEPTH_CONV SYM_CONV) THEN STRIP_TAC THEN ASM_REWRITE_TAC[REAL_ENTIRE] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[]);;
(* ------------------------------------------------------------------------- *) (* Tactic version of REAL_ARITH. *) (* ------------------------------------------------------------------------- *) let REAL_ARITH_TAC = CONV_TAC REAL_ARITH;; (* ------------------------------------------------------------------------- *) (* Prove all the linear theorems we can blow away automatically. *) (* ------------------------------------------------------------------------- *)
let REAL_EQ_ADD_LCANCEL_0 = 
prove (`!x y. (x + y = x) <=> (y = &0)`,
REAL_ARITH_TAC);;
let REAL_EQ_ADD_RCANCEL_0 = 
prove (`!x y. (x + y = y) <=> (x = &0)`,
REAL_ARITH_TAC);;
let REAL_LNEG_UNIQ = 
prove (`!x y. (x + y = &0) <=> (x = --y)`,
REAL_ARITH_TAC);;
let REAL_RNEG_UNIQ = 
prove (`!x y. (x + y = &0) <=> (y = --x)`,
REAL_ARITH_TAC);;
let REAL_NEG_LMUL = 
prove (`!x y. --(x * y) = (--x) * y`,
REAL_ARITH_TAC);;
let REAL_NEG_RMUL = 
prove (`!x y. --(x * y) = x * (--y)`,
REAL_ARITH_TAC);;
let REAL_NEGNEG = 
prove (`!x. --(--x) = x`,
REAL_ARITH_TAC);;
let REAL_NEG_MUL2 = 
prove (`!x y. (--x) * (--y) = x * y`,
REAL_ARITH_TAC);;
let REAL_LT_LADD = 
prove (`!x y z. (x + y) < (x + z) <=> y < z`,
REAL_ARITH_TAC);;
let REAL_LT_RADD = 
prove (`!x y z. (x + z) < (y + z) <=> x < y`,
REAL_ARITH_TAC);;
let REAL_LT_ANTISYM = 
prove (`!x y. ~(x < y /\ y < x)`,
REAL_ARITH_TAC);;
let REAL_LT_GT = 
prove (`!x y. x < y ==> ~(y < x)`,
REAL_ARITH_TAC);;
let REAL_NOT_EQ = 
prove (`!x y. ~(x = y) <=> x < y \/ y < x`,
REAL_ARITH_TAC);;
let REAL_NOT_LE = 
prove (`!x y. ~(x <= y) <=> y < x`,
REAL_ARITH_TAC);;
let REAL_LET_ANTISYM = 
prove (`!x y. ~(x <= y /\ y < x)`,
REAL_ARITH_TAC);;
let REAL_NEG_LT0 = 
prove (`!x. (--x) < &0 <=> &0 < x`,
REAL_ARITH_TAC);;
let REAL_NEG_GT0 = 
prove (`!x. &0 < (--x) <=> x < &0`,
REAL_ARITH_TAC);;
let REAL_NEG_LE0 = 
prove (`!x. (--x) <= &0 <=> &0 <= x`,
REAL_ARITH_TAC);;
let REAL_NEG_GE0 = 
prove (`!x. &0 <= (--x) <=> x <= &0`,
REAL_ARITH_TAC);;
let REAL_LT_TOTAL = 
prove (`!x y. (x = y) \/ x < y \/ y < x`,
REAL_ARITH_TAC);;
let REAL_LT_NEGTOTAL = 
prove (`!x. (x = &0) \/ (&0 < x) \/ (&0 < --x)`,
REAL_ARITH_TAC);;
let REAL_LE_01 = 
prove (`&0 <= &1`,
REAL_ARITH_TAC);;
let REAL_LT_01 = 
prove (`&0 < &1`,
REAL_ARITH_TAC);;
let REAL_LE_LADD = 
prove (`!x y z. (x + y) <= (x + z) <=> y <= z`,
REAL_ARITH_TAC);;
let REAL_LE_RADD = 
prove (`!x y z. (x + z) <= (y + z) <=> x <= y`,
REAL_ARITH_TAC);;
let REAL_LT_ADD2 = 
prove (`!w x y z. w < x /\ y < z ==> (w + y) < (x + z)`,
REAL_ARITH_TAC);;
let REAL_LE_ADD2 = 
prove (`!w x y z. w <= x /\ y <= z ==> (w + y) <= (x + z)`,
REAL_ARITH_TAC);;
let REAL_LT_LNEG = 
prove (`!x y. --x < y <=> &0 < x + y`,
REWRITE_TAC[real_lt; REAL_LE_RNEG; REAL_ADD_AC]);;
let REAL_LT_RNEG = 
prove (`!x y. x < --y <=> x + y < &0`,
REWRITE_TAC[real_lt; REAL_LE_LNEG; REAL_ADD_AC]);;
let REAL_LT_ADDNEG = 
prove (`!x y z. y < (x + (--z)) <=> (y + z) < x`,
REAL_ARITH_TAC);;
let REAL_LT_ADDNEG2 = 
prove (`!x y z. (x + (--y)) < z <=> x < (z + y)`,
REAL_ARITH_TAC);;
let REAL_LT_ADD1 = 
prove (`!x y. x <= y ==> x < (y + &1)`,
REAL_ARITH_TAC);;
let REAL_SUB_ADD = 
prove (`!x y. (x - y) + y = x`,
REAL_ARITH_TAC);;
let REAL_SUB_ADD2 = 
prove (`!x y. y + (x - y) = x`,
REAL_ARITH_TAC);;
let REAL_SUB_REFL = 
prove (`!x. x - x = &0`,
REAL_ARITH_TAC);;
let REAL_LE_DOUBLE = 
prove (`!x. &0 <= x + x <=> &0 <= x`,
REAL_ARITH_TAC);;
let REAL_LE_NEGL = 
prove (`!x. (--x <= x) <=> (&0 <= x)`,
REAL_ARITH_TAC);;
let REAL_LE_NEGR = 
prove (`!x. (x <= --x) <=> (x <= &0)`,
REAL_ARITH_TAC);;
let REAL_NEG_EQ_0 = 
prove (`!x. (--x = &0) <=> (x = &0)`,
REAL_ARITH_TAC);;
let REAL_ADD_SUB = 
prove (`!x y. (x + y) - x = y`,
REAL_ARITH_TAC);;
let REAL_NEG_EQ = 
prove (`!x y. (--x = y) <=> (x = --y)`,
REAL_ARITH_TAC);;
let REAL_NEG_MINUS1 = 
prove (`!x. --x = (--(&1)) * x`,
REAL_ARITH_TAC);;
let REAL_LT_IMP_NE = 
prove (`!x y. x < y ==> ~(x = y)`,
REAL_ARITH_TAC);;
let REAL_LE_ADDR = 
prove (`!x y. x <= x + y <=> &0 <= y`,
REAL_ARITH_TAC);;
let REAL_LE_ADDL = 
prove (`!x y. y <= x + y <=> &0 <= x`,
REAL_ARITH_TAC);;
let REAL_LT_ADDR = 
prove (`!x y. x < x + y <=> &0 < y`,
REAL_ARITH_TAC);;
let REAL_LT_ADDL = 
prove (`!x y. y < x + y <=> &0 < x`,
REAL_ARITH_TAC);;
let REAL_SUB_SUB = 
prove (`!x y. (x - y) - x = --y`,
REAL_ARITH_TAC);;
let REAL_LT_ADD_SUB = 
prove (`!x y z. (x + y) < z <=> x < (z - y)`,
REAL_ARITH_TAC);;
let REAL_LT_SUB_RADD = 
prove (`!x y z. (x - y) < z <=> x < z + y`,
REAL_ARITH_TAC);;
let REAL_LT_SUB_LADD = 
prove (`!x y z. x < (y - z) <=> (x + z) < y`,
REAL_ARITH_TAC);;
let REAL_LE_SUB_LADD = 
prove (`!x y z. x <= (y - z) <=> (x + z) <= y`,
REAL_ARITH_TAC);;
let REAL_LE_SUB_RADD = 
prove (`!x y z. (x - y) <= z <=> x <= z + y`,
REAL_ARITH_TAC);;
let REAL_LT_NEG = 
prove (`!x y. --x < --y <=> y < x`,
REAL_ARITH_TAC);;
let REAL_LE_NEG = 
prove (`!x y. --x <= --y <=> y <= x`,
REAL_ARITH_TAC);;
let REAL_ADD2_SUB2 = 
prove (`!a b c d. (a + b) - (c + d) = (a - c) + (b - d)`,
REAL_ARITH_TAC);;
let REAL_SUB_LZERO = 
prove (`!x. &0 - x = --x`,
REAL_ARITH_TAC);;
let REAL_SUB_RZERO = 
prove (`!x. x - &0 = x`,
REAL_ARITH_TAC);;
let REAL_LET_ADD2 = 
prove (`!w x y z. w <= x /\ y < z ==> (w + y) < (x + z)`,
REAL_ARITH_TAC);;
let REAL_LTE_ADD2 = 
prove (`!w x y z. w < x /\ y <= z ==> w + y < x + z`,
REAL_ARITH_TAC);;
let REAL_SUB_LNEG = 
prove (`!x y. (--x) - y = --(x + y)`,
REAL_ARITH_TAC);;
let REAL_SUB_RNEG = 
prove (`!x y. x - (--y) = x + y`,
REAL_ARITH_TAC);;
let REAL_SUB_NEG2 = 
prove (`!x y. (--x) - (--y) = y - x`,
REAL_ARITH_TAC);;
let REAL_SUB_TRIANGLE = 
prove (`!a b c. (a - b) + (b - c) = a - c`,
REAL_ARITH_TAC);;
let REAL_EQ_SUB_LADD = 
prove (`!x y z. (x = y - z) <=> (x + z = y)`,
REAL_ARITH_TAC);;
let REAL_EQ_SUB_RADD = 
prove (`!x y z. (x - y = z) <=> (x = z + y)`,
REAL_ARITH_TAC);;
let REAL_SUB_SUB2 = 
prove (`!x y. x - (x - y) = y`,
REAL_ARITH_TAC);;
let REAL_ADD_SUB2 = 
prove (`!x y. x - (x + y) = --y`,
REAL_ARITH_TAC);;
let REAL_EQ_IMP_LE = 
prove (`!x y. (x = y) ==> x <= y`,
REAL_ARITH_TAC);;
let REAL_POS_NZ = 
prove (`!x. &0 < x ==> ~(x = &0)`,
REAL_ARITH_TAC);;
let REAL_DIFFSQ = 
prove (`!x y. (x + y) * (x - y) = (x * x) - (y * y)`,
REAL_ARITH_TAC);;
let REAL_EQ_NEG2 = 
prove (`!x y. (--x = --y) <=> (x = y)`,
REAL_ARITH_TAC);;
let REAL_LT_NEG2 = 
prove (`!x y. --x < --y <=> y < x`,
REAL_ARITH_TAC);;
let REAL_SUB_LDISTRIB = 
prove (`!x y z. x * (y - z) = x * y - x * z`,
REAL_ARITH_TAC);;
let REAL_SUB_RDISTRIB = 
prove (`!x y z. (x - y) * z = x * z - y * z`,
REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *) (* Theorems about "abs". *) (* ------------------------------------------------------------------------- *)
let REAL_ABS_ZERO = 
prove (`!x. (abs(x) = &0) <=> (x = &0)`,
REAL_ARITH_TAC);;
let REAL_ABS_0 = 
prove (`abs(&0) = &0`,
REAL_ARITH_TAC);;
let REAL_ABS_1 = 
prove (`abs(&1) = &1`,
REAL_ARITH_TAC);;
let REAL_ABS_TRIANGLE = 
prove (`!x y. abs(x + y) <= abs(x) + abs(y)`,
REAL_ARITH_TAC);;
let REAL_ABS_TRIANGLE_LE = 
prove (`!x y z.abs(x) + abs(y - x) <= z ==> abs(y) <= z`,
REAL_ARITH_TAC);;
let REAL_ABS_TRIANGLE_LT = 
prove (`!x y z.abs(x) + abs(y - x) < z ==> abs(y) < z`,
REAL_ARITH_TAC);;
let REAL_ABS_POS = 
prove (`!x. &0 <= abs(x)`,
REAL_ARITH_TAC);;
let REAL_ABS_SUB = 
prove (`!x y. abs(x - y) = abs(y - x)`,
REAL_ARITH_TAC);;
let REAL_ABS_NZ = 
prove (`!x. ~(x = &0) <=> &0 < abs(x)`,
REAL_ARITH_TAC);;
let REAL_ABS_ABS = 
prove (`!x. abs(abs(x)) = abs(x)`,
REAL_ARITH_TAC);;
let REAL_ABS_LE = 
prove (`!x. x <= abs(x)`,
REAL_ARITH_TAC);;
let REAL_ABS_REFL = 
prove (`!x. (abs(x) = x) <=> &0 <= x`,
REAL_ARITH_TAC);;
let REAL_ABS_BETWEEN = 
prove (`!x y d. &0 < d /\ ((x - d) < y) /\ (y < (x + d)) <=> abs(y - x) < d`,
REAL_ARITH_TAC);;
let REAL_ABS_BOUND = 
prove (`!x y d. abs(x - y) < d ==> y < (x + d)`,
REAL_ARITH_TAC);;
let REAL_ABS_STILLNZ = 
prove (`!x y. abs(x - y) < abs(y) ==> ~(x = &0)`,
REAL_ARITH_TAC);;
let REAL_ABS_CASES = 
prove (`!x. (x = &0) \/ &0 < abs(x)`,
REAL_ARITH_TAC);;
let REAL_ABS_BETWEEN1 = 
prove (`!x y z. x < z /\ (abs(y - x)) < (z - x) ==> y < z`,
REAL_ARITH_TAC);;
let REAL_ABS_SIGN = 
prove (`!x y. abs(x - y) < y ==> &0 < x`,
REAL_ARITH_TAC);;
let REAL_ABS_SIGN2 = 
prove (`!x y. abs(x - y) < --y ==> x < &0`,
REAL_ARITH_TAC);;
let REAL_ABS_CIRCLE = 
prove (`!x y h. abs(h) < (abs(y) - abs(x)) ==> abs(x + h) < abs(y)`,
REAL_ARITH_TAC);;
let REAL_SUB_ABS = 
prove (`!x y. (abs(x) - abs(y)) <= abs(x - y)`,
REAL_ARITH_TAC);;
let REAL_ABS_SUB_ABS = 
prove (`!x y. abs(abs(x) - abs(y)) <= abs(x - y)`,
REAL_ARITH_TAC);;
let REAL_ABS_BETWEEN2 = 
prove (`!x0 x y0 y. x0 < y0 /\ &2 * abs(x - x0) < (y0 - x0) /\ &2 * abs(y - y0) < (y0 - x0) ==> x < y`,
REAL_ARITH_TAC);;
let REAL_ABS_BOUNDS = 
prove (`!x k. abs(x) <= k <=> --k <= x /\ x <= k`,
REAL_ARITH_TAC);;
let REAL_BOUNDS_LE = 
prove (`!x k. --k <= x /\ x <= k <=> abs(x) <= k`,
REAL_ARITH_TAC);;
let REAL_BOUNDS_LT = 
prove (`!x k. --k < x /\ x < k <=> abs(x) < k`,
REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *) (* Theorems about max and min. *) (* ------------------------------------------------------------------------- *)
let REAL_MIN_MAX = 
prove (`!x y. min x y = --(max (--x) (--y))`,
REAL_ARITH_TAC);;
let REAL_MAX_MIN = 
prove (`!x y. max x y = --(min (--x) (--y))`,
REAL_ARITH_TAC);;
let REAL_MAX_MAX = 
prove (`!x y. x <= max x y /\ y <= max x y`,
REAL_ARITH_TAC);;
let REAL_MIN_MIN = 
prove (`!x y. min x y <= x /\ min x y <= y`,
REAL_ARITH_TAC);;
let REAL_MAX_SYM = 
prove (`!x y. max x y = max y x`,
REAL_ARITH_TAC);;
let REAL_MIN_SYM = 
prove (`!x y. min x y = min y x`,
REAL_ARITH_TAC);;
let REAL_LE_MAX = 
prove (`!x y z. z <= max x y <=> z <= x \/ z <= y`,
REAL_ARITH_TAC);;
let REAL_LE_MIN = 
prove (`!x y z. z <= min x y <=> z <= x /\ z <= y`,
REAL_ARITH_TAC);;
let REAL_LT_MAX = 
prove (`!x y z. z < max x y <=> z < x \/ z < y`,
REAL_ARITH_TAC);;
let REAL_LT_MIN = 
prove (`!x y z. z < min x y <=> z < x /\ z < y`,
REAL_ARITH_TAC);;
let REAL_MAX_LE = 
prove (`!x y z. max x y <= z <=> x <= z /\ y <= z`,
REAL_ARITH_TAC);;
let REAL_MIN_LE = 
prove (`!x y z. min x y <= z <=> x <= z \/ y <= z`,
REAL_ARITH_TAC);;
let REAL_MAX_LT = 
prove (`!x y z. max x y < z <=> x < z /\ y < z`,
REAL_ARITH_TAC);;
let REAL_MIN_LT = 
prove (`!x y z. min x y < z <=> x < z \/ y < z`,
REAL_ARITH_TAC);;
let REAL_MAX_ASSOC = 
prove (`!x y z. max x (max y z) = max (max x y) z`,
REAL_ARITH_TAC);;
let REAL_MIN_ASSOC = 
prove (`!x y z. min x (min y z) = min (min x y) z`,
REAL_ARITH_TAC);;
let REAL_MAX_ACI = 
prove (`(max x y = max y x) /\ (max (max x y) z = max x (max y z)) /\ (max x (max y z) = max y (max x z)) /\ (max x x = x) /\ (max x (max x y) = max x y)`,
REAL_ARITH_TAC);;
let REAL_MIN_ACI = 
prove (`(min x y = min y x) /\ (min (min x y) z = min x (min y z)) /\ (min x (min y z) = min y (min x z)) /\ (min x x = x) /\ (min x (min x y) = min x y)`,
REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *) (* To simplify backchaining, just as in the natural number case. *) (* ------------------------------------------------------------------------- *) let REAL_LE_IMP = let pth = PURE_ONCE_REWRITE_RULE[IMP_CONJ] REAL_LE_TRANS in fun th -> GEN_ALL(MATCH_MP pth (SPEC_ALL th));; let REAL_LET_IMP = let pth = PURE_ONCE_REWRITE_RULE[IMP_CONJ] REAL_LET_TRANS in fun th -> GEN_ALL(MATCH_MP pth (SPEC_ALL th));; (* ------------------------------------------------------------------------- *) (* Now a bit of nonlinear stuff. *) (* ------------------------------------------------------------------------- *)
let REAL_ABS_MUL = 
prove (`!x y. abs(x * y) = abs(x) * abs(y)`,
REPEAT GEN_TAC THEN DISJ_CASES_TAC (SPEC `x:real` REAL_LE_NEGTOTAL) THENL [ALL_TAC; GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [GSYM REAL_ABS_NEG]] THEN (DISJ_CASES_TAC (SPEC `y:real` REAL_LE_NEGTOTAL) THENL [ALL_TAC; GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [GSYM REAL_ABS_NEG]]) THEN ASSUM_LIST(MP_TAC o MATCH_MP REAL_LE_MUL o end_itlist CONJ o rev) THEN REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN DISCH_TAC THENL [ALL_TAC; GEN_REWRITE_TAC LAND_CONV [GSYM REAL_ABS_NEG]; GEN_REWRITE_TAC LAND_CONV [GSYM REAL_ABS_NEG]; ALL_TAC] THEN ASM_REWRITE_TAC[real_abs; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG]);;
let REAL_POW_LE = 
prove (`!x n. &0 <= x ==> &0 <= x pow n`,
REPEAT STRIP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN REWRITE_TAC[real_pow; REAL_POS] THEN MATCH_MP_TAC REAL_LE_MUL THEN ASM_REWRITE_TAC[]);;
let REAL_POW_LT = 
prove (`!x n. &0 < x ==> &0 < x pow n`,
REPEAT STRIP_TAC THEN SPEC_TAC(`n:num`,`n:num`) THEN INDUCT_TAC THEN REWRITE_TAC[real_pow; REAL_LT_01] THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[]);;
let REAL_ABS_POW = 
prove (`!x n. abs(x pow n) = abs(x) pow n`,
GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[real_pow; REAL_ABS_NUM; REAL_ABS_MUL]);;
let REAL_LE_LMUL = 
prove (`!x y z. &0 <= x /\ y <= z ==> x * y <= x * z`,
ONCE_REWRITE_TAC[REAL_ARITH `x <= y <=> &0 <= y - x`] THEN REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; REAL_SUB_RZERO; REAL_LE_MUL]);;
let REAL_LE_RMUL = 
prove (`!x y z. x <= y /\ &0 <= z ==> x * z <= y * z`,
MESON_TAC[REAL_MUL_SYM; REAL_LE_LMUL]);;
let REAL_LT_LMUL = 
prove (`!x y z. &0 < x /\ y < z ==> x * y < x * z`,
ONCE_REWRITE_TAC[REAL_ARITH `x < y <=> &0 < y - x`] THEN REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; REAL_SUB_RZERO; REAL_LT_MUL]);;
let REAL_LT_RMUL = 
prove (`!x y z. x < y /\ &0 < z ==> x * z < y * z`,
MESON_TAC[REAL_MUL_SYM; REAL_LT_LMUL]);;
let REAL_EQ_MUL_LCANCEL = 
prove (`!x y z. (x * y = x * z) <=> (x = &0) \/ (y = z)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[REAL_ARITH `(x = y) <=> (x - y = &0)`] THEN REWRITE_TAC[GSYM REAL_SUB_LDISTRIB; REAL_ENTIRE; REAL_SUB_RZERO]);;
let REAL_EQ_MUL_RCANCEL = 
prove (`!x y z. (x * z = y * z) <=> (x = y) \/ (z = &0)`,
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_EQ_MUL_LCANCEL] THEN MESON_TAC[]);;
let REAL_MUL_LINV_UNIQ = 
prove (`!x y. (x * y = &1) ==> (inv(y) = x)`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `y = &0` THEN ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_OF_NUM_EQ; ARITH_EQ] THEN FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP REAL_MUL_LINV) THEN ASM_REWRITE_TAC[REAL_EQ_MUL_RCANCEL] THEN DISCH_THEN(ACCEPT_TAC o SYM));;
let REAL_MUL_RINV_UNIQ = 
prove (`!x y. (x * y = &1) ==> (inv(x) = y)`,
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN MATCH_ACCEPT_TAC REAL_MUL_LINV_UNIQ);;
let REAL_INV_INV = 
prove (`!x. inv(inv x) = x`,
GEN_TAC THEN ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[REAL_INV_0] THEN MATCH_MP_TAC REAL_MUL_RINV_UNIQ THEN MATCH_MP_TAC REAL_MUL_LINV THEN ASM_REWRITE_TAC[]);;
let REAL_EQ_INV2 = 
prove (`!x y. inv(x) = inv(y) <=> x = y`,
MESON_TAC[REAL_INV_INV]);;
let REAL_INV_EQ_0 = 
prove (`!x. inv(x) = &0 <=> x = &0`,
GEN_TAC THEN EQ_TAC THEN DISCH_TAC THEN ASM_REWRITE_TAC[REAL_INV_0] THEN ONCE_REWRITE_TAC[GSYM REAL_INV_INV] THEN ASM_REWRITE_TAC[REAL_INV_0]);;
let REAL_LT_INV = 
prove (`!x. &0 < x ==> &0 < inv(x)`,
GEN_TAC THEN REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC `inv(x)` REAL_LT_NEGTOTAL) THEN ASM_REWRITE_TAC[] THENL [RULE_ASSUM_TAC(REWRITE_RULE[REAL_INV_EQ_0]) THEN ASM_REWRITE_TAC[]; DISCH_TAC THEN SUBGOAL_THEN `&0 < --(inv x) * x` MP_TAC THENL [MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[]; REWRITE_TAC[REAL_MUL_LNEG]]] THEN SUBGOAL_THEN `inv(x) * x = &1` SUBST1_TAC THENL [MATCH_MP_TAC REAL_MUL_LINV THEN UNDISCH_TAC `&0 < x` THEN REAL_ARITH_TAC; REWRITE_TAC[REAL_LT_RNEG; REAL_ADD_LID; REAL_OF_NUM_LT; ARITH]]);;
let REAL_LT_INV_EQ = 
prove (`!x. &0 < inv x <=> &0 < x`,
GEN_TAC THEN EQ_TAC THEN REWRITE_TAC[REAL_LT_INV] THEN GEN_REWRITE_TAC (funpow 2 RAND_CONV) [GSYM REAL_INV_INV] THEN REWRITE_TAC[REAL_LT_INV]);;
let REAL_INV_NEG = 
prove (`!x. inv(--x) = --(inv x)`,
GEN_TAC THEN ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[REAL_NEG_0; REAL_INV_0] THEN MATCH_MP_TAC REAL_MUL_LINV_UNIQ THEN REWRITE_TAC[REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN MATCH_MP_TAC REAL_MUL_LINV THEN ASM_REWRITE_TAC[]);;
let REAL_LE_INV_EQ = 
prove (`!x. &0 <= inv x <=> &0 <= x`,
REWRITE_TAC[REAL_LE_LT; REAL_LT_INV_EQ; REAL_INV_EQ_0] THEN MESON_TAC[REAL_INV_EQ_0]);;
let REAL_LE_INV = 
prove (`!x. &0 <= x ==> &0 <= inv(x)`,
REWRITE_TAC[REAL_LE_INV_EQ]);;
let REAL_MUL_RINV = 
prove (`!x. ~(x = &0) ==> (x * inv(x) = &1)`,
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_MUL_LINV]);;
let REAL_INV_1 = 
prove (`inv(&1) = &1`,
MATCH_MP_TAC REAL_MUL_RINV_UNIQ THEN REWRITE_TAC[REAL_MUL_LID]);;
let REAL_INV_EQ_1 = 
prove (`!x. inv(x) = &1 <=> x = &1`,
MESON_TAC[REAL_INV_INV; REAL_INV_1]);;
let REAL_DIV_1 = 
prove (`!x. x / &1 = x`,
REWRITE_TAC[real_div; REAL_INV_1; REAL_MUL_RID]);;
let REAL_DIV_REFL = 
prove (`!x. ~(x = &0) ==> (x / x = &1)`,
GEN_TAC THEN REWRITE_TAC[real_div; REAL_MUL_RINV]);;
let REAL_DIV_RMUL = 
prove (`!x y. ~(y = &0) ==> ((x / y) * y = x)`,
SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_RID]);;
let REAL_DIV_LMUL = 
prove (`!x y. ~(y = &0) ==> (y * (x / y) = x)`,
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_DIV_RMUL]);;
let REAL_ABS_INV = 
prove (`!x. abs(inv x) = inv(abs x)`,
GEN_TAC THEN CONV_TAC SYM_CONV THEN ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[REAL_INV_0; REAL_ABS_0] THEN MATCH_MP_TAC REAL_MUL_RINV_UNIQ THEN REWRITE_TAC[GSYM REAL_ABS_MUL] THEN POP_ASSUM(SUBST1_TAC o MATCH_MP REAL_MUL_RINV) THEN REWRITE_TAC[REAL_ABS_1]);;
let REAL_ABS_DIV = 
prove (`!x y. abs(x / y) = abs(x) / abs(y)`,
let REAL_INV_MUL = 
prove (`!x y. inv(x * y) = inv(x) * inv(y)`,
REPEAT GEN_TAC THEN MAP_EVERY ASM_CASES_TAC [`x = &0`; `y = &0`] THEN ASM_REWRITE_TAC[REAL_INV_0; REAL_MUL_LZERO; REAL_MUL_RZERO] THEN MATCH_MP_TAC REAL_MUL_LINV_UNIQ THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b) * (c * d) = (a * c) * (b * d)`] THEN EVERY_ASSUM(SUBST1_TAC o MATCH_MP REAL_MUL_LINV) THEN REWRITE_TAC[REAL_MUL_LID]);;
let REAL_INV_DIV = 
prove (`!x y. inv(x / y) = y / x`,
REWRITE_TAC[real_div; REAL_INV_INV; REAL_INV_MUL] THEN MATCH_ACCEPT_TAC REAL_MUL_SYM);;
let REAL_POW_MUL = 
prove (`!x y n. (x * y) pow n = (x pow n) * (y pow n)`,
GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[real_pow; REAL_MUL_LID; REAL_MUL_AC]);;
let REAL_POW_INV = 
prove (`!x n. (inv x) pow n = inv(x pow n)`,
GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[real_pow; REAL_INV_1; REAL_INV_MUL]);;
let REAL_INV_POW = 
prove (`!x n. inv(x pow n) = (inv x) pow n`,
REWRITE_TAC[REAL_POW_INV]);;
let REAL_POW_DIV = 
prove (`!x y n. (x / y) pow n = (x pow n) / (y pow n)`,
let REAL_DIV_EQ_0 = 
prove (`!x y. x / y = &0 <=> x = &0 \/ y = &0`,
let REAL_POW_ADD = 
prove (`!x m n. x pow (m + n) = x pow m * x pow n`,
GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_CLAUSES; real_pow; REAL_MUL_LID; REAL_MUL_ASSOC]);;
let REAL_POW_NZ = 
prove (`!x n. ~(x = &0) ==> ~(x pow n = &0)`,
GEN_TAC THEN INDUCT_TAC THEN REWRITE_TAC[real_pow; REAL_OF_NUM_EQ; ARITH] THEN ASM_MESON_TAC[REAL_ENTIRE]);;
let REAL_POW_SUB = 
prove (`!x m n. ~(x = &0) /\ m <= n ==> (x pow (n - m) = x pow n / x pow m)`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[LE_EXISTS] THEN DISCH_THEN(CHOOSE_THEN SUBST1_TAC) THEN REWRITE_TAC[ADD_SUB2] THEN REWRITE_TAC[REAL_POW_ADD] THEN REWRITE_TAC[real_div] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN REWRITE_TAC[REAL_MUL_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_MUL_LINV THEN MATCH_MP_TAC REAL_POW_NZ THEN ASM_REWRITE_TAC[]);;
let REAL_LT_IMP_NZ = 
prove (`!x. &0 < x ==> ~(x = &0)`,
REAL_ARITH_TAC);;
let REAL_LT_LCANCEL_IMP = 
prove (`!x y z. &0 < x /\ x * y < x * z ==> y < z`,
REPEAT GEN_TAC THEN DISCH_THEN(fun th -> ASSUME_TAC(CONJUNCT1 th) THEN MP_TAC th) THEN DISCH_THEN (MP_TAC o uncurry CONJ o (MATCH_MP REAL_LT_INV F_F I) o CONJ_PAIR) THEN DISCH_THEN(MP_TAC o MATCH_MP REAL_LT_LMUL) THEN POP_ASSUM(ASSUME_TAC o MATCH_MP REAL_MUL_LINV o MATCH_MP REAL_LT_IMP_NZ) THEN ASM_REWRITE_TAC[REAL_MUL_ASSOC; REAL_MUL_LID]);;
let REAL_LT_RCANCEL_IMP = 
prove (`!x y z. &0 < z /\ x * z < y * z ==> x < y`,
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_LT_LCANCEL_IMP]);;
let REAL_LE_LCANCEL_IMP = 
prove (`!x y z. &0 < x /\ x * y <= x * z ==> y <= z`,
REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT; REAL_EQ_MUL_LCANCEL] THEN ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[REAL_LT_REFL] THEN STRIP_TAC THEN ASM_REWRITE_TAC[] THEN DISJ1_TAC THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `x:real` THEN ASM_REWRITE_TAC[]);;
let REAL_LE_RCANCEL_IMP = 
prove (`!x y z. &0 < z /\ x * z <= y * z ==> x <= y`,
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_LE_LCANCEL_IMP]);;
let REAL_LE_RMUL_EQ = 
prove (`!x y z. &0 < z ==> (x * z <= y * z <=> x <= y)`,
let REAL_LE_LMUL_EQ = 
prove (`!x y z. &0 < z ==> (z * x <= z * y <=> x <= y)`,
MESON_TAC[REAL_LE_RMUL_EQ; REAL_MUL_SYM]);;
let REAL_LT_RMUL_EQ = 
prove (`!x y z. &0 < z ==> (x * z < y * z <=> x < y)`,
SIMP_TAC[GSYM REAL_NOT_LE; REAL_LE_RMUL_EQ]);;
let REAL_LT_LMUL_EQ = 
prove (`!x y z. &0 < z ==> (z * x < z * y <=> x < y)`,
SIMP_TAC[GSYM REAL_NOT_LE; REAL_LE_LMUL_EQ]);;
let REAL_LE_MUL_EQ = 
prove (`(!x y. &0 < x ==> (&0 <= x * y <=> &0 <= y)) /\ (!x y. &0 < y ==> (&0 <= x * y <=> &0 <= x))`,
let REAL_LT_MUL_EQ = 
prove (`(!x y. &0 < x ==> (&0 < x * y <=> &0 < y)) /\ (!x y. &0 < y ==> (&0 < x * y <=> &0 < x))`,
let REAL_MUL_POS_LT = 
prove (`!x y. &0 < x * y <=> &0 < x /\ &0 < y \/ x < &0 /\ y < &0`,
REPEAT STRIP_TAC THEN STRIP_ASSUME_TAC(SPEC `x:real` REAL_LT_NEGTOTAL) THEN STRIP_ASSUME_TAC(SPEC `y:real` REAL_LT_NEGTOTAL) THEN ASM_REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_LT_REFL] THEN ASSUM_LIST(MP_TAC o MATCH_MP REAL_LT_MUL o end_itlist CONJ) THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC);;
let REAL_MUL_POS_LE = 
prove (`!x y. &0 <= x * y <=> x = &0 \/ y = &0 \/ &0 < x /\ &0 < y \/ x < &0 /\ y < &0`,
REWRITE_TAC[REAL_ARITH `&0 <= x <=> x = &0 \/ &0 < x`] THEN REWRITE_TAC[REAL_MUL_POS_LT; REAL_ENTIRE] THEN REAL_ARITH_TAC);;
let REAL_LE_RDIV_EQ = 
prove (`!x y z. &0 < z ==> (x <= y / z <=> x * z <= y)`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [GSYM(MATCH_MP REAL_LE_RMUL_EQ th)]) THEN ASM_SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_RID; REAL_LT_IMP_NZ]);;
let REAL_LE_LDIV_EQ = 
prove (`!x y z. &0 < z ==> (x / z <= y <=> x <= y * z)`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [GSYM(MATCH_MP REAL_LE_RMUL_EQ th)]) THEN ASM_SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_MUL_RID; REAL_LT_IMP_NZ]);;
let REAL_LT_RDIV_EQ = 
prove (`!x y z. &0 < z ==> (x < y / z <=> x * z < y)`,
SIMP_TAC[GSYM REAL_NOT_LE; REAL_LE_LDIV_EQ]);;
let REAL_LT_LDIV_EQ = 
prove (`!x y z. &0 < z ==> (x / z < y <=> x < y * z)`,
SIMP_TAC[GSYM REAL_NOT_LE; REAL_LE_RDIV_EQ]);;
let REAL_EQ_RDIV_EQ = 
prove (`!x y z. &0 < z ==> ((x = y / z) <=> (x * z = y))`,
REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ]);;
let REAL_EQ_LDIV_EQ = 
prove (`!x y z. &0 < z ==> ((x / z = y) <=> (x = y * z))`,
REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LE_LDIV_EQ]);;
let REAL_LT_DIV2_EQ = 
prove (`!x y z. &0 < z ==> (x / z < y / z <=> x < y)`,
let REAL_LE_DIV2_EQ = 
prove (`!x y z. &0 < z ==> (x / z <= y / z <=> x <= y)`,
let REAL_MUL_2 = 
prove (`!x. &2 * x = x + x`,
REAL_ARITH_TAC);;
let REAL_POW_EQ_0 = 
prove (`!x n. (x pow n = &0) <=> (x = &0) /\ ~(n = 0)`,
GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[NOT_SUC; real_pow; REAL_ENTIRE] THENL [REAL_ARITH_TAC; CONV_TAC TAUT]);;
let REAL_LE_MUL2 = 
prove (`!w x y z. &0 <= w /\ w <= x /\ &0 <= y /\ y <= z ==> w * y <= x * z`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `w * z` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_LMUL; MATCH_MP_TAC REAL_LE_RMUL] THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `y:real` THEN ASM_REWRITE_TAC[]);;
let REAL_LT_MUL2 = 
prove (`!w x y z. &0 <= w /\ w < x /\ &0 <= y /\ y < z ==> w * y < x * z`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `w * z` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_LMUL; MATCH_MP_TAC REAL_LT_RMUL] THEN ASM_REWRITE_TAC[] THENL [MATCH_MP_TAC REAL_LT_IMP_LE THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `y:real` THEN ASM_REWRITE_TAC[]]);;
let REAL_LT_SQUARE = 
prove (`!x. (&0 < x * x) <=> ~(x = &0)`,
GEN_TAC THEN REWRITE_TAC[REAL_LT_LE; REAL_LE_SQUARE] THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [EQ_SYM_EQ] THEN REWRITE_TAC[REAL_ENTIRE]);;
let REAL_POW_1 = 
prove (`!x. x pow 1 = x`,
REWRITE_TAC[num_CONV `1`] THEN REWRITE_TAC[real_pow; REAL_MUL_RID]);;
let REAL_POW_ONE = 
prove (`!n. &1 pow n = &1`,
INDUCT_TAC THEN ASM_REWRITE_TAC[real_pow; REAL_MUL_LID]);;
let REAL_LT_INV2 = 
prove (`!x y. &0 < x /\ x < y ==> inv(y) < inv(x)`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LT_RCANCEL_IMP THEN EXISTS_TAC `x * y` THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LT_MUL THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC; SUBGOAL_THEN `(inv x * x = &1) /\ (inv y * y = &1)` ASSUME_TAC THENL [CONJ_TAC THEN MATCH_MP_TAC REAL_MUL_LINV THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC; ASM_REWRITE_TAC[REAL_MUL_ASSOC; REAL_MUL_LID] THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN ASM_REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_MUL_RID]]]);;
let REAL_LE_INV2 = 
prove (`!x y. &0 < x /\ x <= y ==> inv(y) <= inv(x)`,
REPEAT GEN_TAC THEN REWRITE_TAC[REAL_LE_LT] THEN ASM_CASES_TAC `x:real = y` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THEN DISJ1_TAC THEN MATCH_MP_TAC REAL_LT_INV2 THEN ASM_REWRITE_TAC[]);;
let REAL_LT_LINV = 
prove (`!x y. &0 < y /\ inv y < x ==> inv x < y`,
REPEAT STRIP_TAC THEN MP_TAC (SPEC `y:real` REAL_LT_INV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (SPECL [`(inv y:real)`; `x:real`] REAL_LT_INV2) THEN ASM_REWRITE_TAC[REAL_INV_INV]);;
let REAL_LT_RINV = 
prove (`!x y. &0 < x /\ x < inv y ==> y < inv x`,
REPEAT STRIP_TAC THEN MP_TAC (SPEC `x:real` REAL_LT_INV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (SPECL [`x:real`; `inv y:real`] REAL_LT_INV2) THEN ASM_REWRITE_TAC[REAL_INV_INV]);;
let REAL_LE_LINV = 
prove (`!x y. &0 < y /\ inv y <= x ==> inv x <= y`,
REPEAT STRIP_TAC THEN MP_TAC (SPEC `y:real` REAL_LT_INV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (SPECL [`(inv y:real)`; `x:real`] REAL_LE_INV2) THEN ASM_REWRITE_TAC[REAL_INV_INV]);;
let REAL_LE_RINV = 
prove (`!x y. &0 < x /\ x <= inv y ==> y <= inv x`,
REPEAT STRIP_TAC THEN MP_TAC (SPEC `x:real` REAL_LT_INV) THEN ASM_REWRITE_TAC[] THEN DISCH_TAC THEN MP_TAC (SPECL [`x:real`; `inv y:real`] REAL_LE_INV2) THEN ASM_REWRITE_TAC[REAL_INV_INV]);;
let REAL_INV_LE_1 = 
prove (`!x. &1 <= x ==> inv(x) <= &1`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_INV_1] THEN MATCH_MP_TAC REAL_LE_INV2 THEN ASM_REWRITE_TAC[REAL_LT_01]);;
let REAL_INV_1_LE = 
prove (`!x. &0 < x /\ x <= &1 ==> &1 <= inv(x)`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_INV_1] THEN MATCH_MP_TAC REAL_LE_INV2 THEN ASM_REWRITE_TAC[REAL_LT_01]);;
let REAL_INV_LT_1 = 
prove (`!x. &1 < x ==> inv(x) < &1`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_INV_1] THEN MATCH_MP_TAC REAL_LT_INV2 THEN ASM_REWRITE_TAC[REAL_LT_01]);;
let REAL_INV_1_LT = 
prove (`!x. &0 < x /\ x < &1 ==> &1 < inv(x)`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_INV_1] THEN MATCH_MP_TAC REAL_LT_INV2 THEN ASM_REWRITE_TAC[REAL_LT_01]);;
let REAL_SUB_INV = 
prove (`!x y. ~(x = &0) /\ ~(y = &0) ==> (inv(x) - inv(y) = (y - x) / (x * y))`,
REWRITE_TAC[real_div; REAL_SUB_RDISTRIB; REAL_INV_MUL] THEN SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_RINV; REAL_MUL_LID] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM real_div] THEN SIMP_TAC[REAL_DIV_LMUL]);;
let REAL_DOWN = 
prove (`!d. &0 < d ==> ?e. &0 < e /\ e < d`,
GEN_TAC THEN DISCH_TAC THEN EXISTS_TAC `d / &2` THEN ASSUME_TAC(REAL_ARITH `&0 < &2`) THEN ASSUME_TAC(MATCH_MP REAL_MUL_LINV (REAL_ARITH `~(&2 = &0)`)) THEN CONJ_TAC THEN MATCH_MP_TAC REAL_LT_RCANCEL_IMP THEN EXISTS_TAC `&2` THEN ASM_REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_MUL_RID] THEN UNDISCH_TAC `&0 < d` THEN REAL_ARITH_TAC);;
let REAL_DOWN2 = 
prove (`!d1 d2. &0 < d1 /\ &0 < d2 ==> ?e. &0 < e /\ e < d1 /\ e < d2`,
REPEAT GEN_TAC THEN STRIP_TAC THEN DISJ_CASES_TAC(SPECL [`d1:real`; `d2:real`] REAL_LE_TOTAL) THENL [MP_TAC(SPEC `d1:real` REAL_DOWN); MP_TAC(SPEC `d2:real` REAL_DOWN)] THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `e:real` STRIP_ASSUME_TAC) THEN EXISTS_TAC `e:real` THEN POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN REAL_ARITH_TAC);;
let REAL_POW_LE2 = 
prove (`!n x y. &0 <= x /\ x <= y ==> x pow n <= y pow n`,
INDUCT_TAC THEN REWRITE_TAC[real_pow; REAL_LE_REFL] THEN REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_MUL2 THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_POW_LE THEN ASM_REWRITE_TAC[]; FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]);;
let REAL_POW_LE_1 = 
prove (`!n x. &1 <= x ==> &1 <= x pow n`,
REPEAT STRIP_TAC THEN MP_TAC(SPECL [`n:num`; `&1`; `x:real`] REAL_POW_LE2) THEN ASM_REWRITE_TAC[REAL_POW_ONE; REAL_POS]);;
let REAL_POW_1_LE = 
prove (`!n x. &0 <= x /\ x <= &1 ==> x pow n <= &1`,
REPEAT STRIP_TAC THEN MP_TAC(SPECL [`n:num`; `x:real`; `&1`] REAL_POW_LE2) THEN ASM_REWRITE_TAC[REAL_POW_ONE]);;
let REAL_POW_MONO = 
prove (`!m n x. &1 <= x /\ m <= n ==> x pow m <= x pow n`,
REPEAT GEN_TAC THEN REWRITE_TAC[LE_EXISTS] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(X_CHOOSE_THEN `d:num` SUBST1_TAC) THEN REWRITE_TAC[REAL_POW_ADD] THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LE_LMUL THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN MATCH_MP_TAC REAL_POW_LE_1 THEN ASM_REWRITE_TAC[]; MATCH_MP_TAC REAL_POW_LE_1 THEN ASM_REWRITE_TAC[]]);;
let REAL_POW_LT2 = 
prove (`!n x y. ~(n = 0) /\ &0 <= x /\ x < y ==> x pow n < y pow n`,
INDUCT_TAC THEN REWRITE_TAC[NOT_SUC; real_pow] THEN REPEAT STRIP_TAC THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[real_pow; REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_REWRITE_TAC[] THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_POW_LE THEN ASM_REWRITE_TAC[]; FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]]);;
let REAL_POW_LT_1 = 
prove (`!n x. ~(n = 0) /\ &1 < x ==> &1 < x pow n`,
REPEAT STRIP_TAC THEN MP_TAC(SPECL [`n:num`; `&1`; `x:real`] REAL_POW_LT2) THEN ASM_REWRITE_TAC[REAL_POW_ONE; REAL_POS]);;
let REAL_POW_1_LT = 
prove (`!n x. ~(n = 0) /\ &0 <= x /\ x < &1 ==> x pow n < &1`,
REPEAT STRIP_TAC THEN MP_TAC(SPECL [`n:num`; `x:real`; `&1`] REAL_POW_LT2) THEN ASM_REWRITE_TAC[REAL_POW_ONE]);;
let REAL_POW_MONO_LT = 
prove (`!m n x. &1 < x /\ m < n ==> x pow m < x pow n`,
REPEAT GEN_TAC THEN REWRITE_TAC[LT_EXISTS] THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN DISCH_THEN(CHOOSE_THEN SUBST_ALL_TAC) THEN REWRITE_TAC[REAL_POW_ADD] THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_RID] THEN MATCH_MP_TAC REAL_LT_LMUL THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_POW_LT THEN MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC `&1` THEN ASM_REWRITE_TAC[REAL_OF_NUM_LT; ARITH]; SPEC_TAC(`d:num`,`d:num`) THEN INDUCT_TAC THEN ONCE_REWRITE_TAC[real_pow] THENL [ASM_REWRITE_TAC[real_pow; REAL_MUL_RID]; ALL_TAC] THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LT_MUL2 THEN ASM_REWRITE_TAC[REAL_OF_NUM_LE; ARITH]]);;
let REAL_POW_POW = 
prove (`!x m n. (x pow m) pow n = x pow (m * n)`,
GEN_TAC THEN GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[real_pow; MULT_CLAUSES; REAL_POW_ADD]);;
let REAL_EQ_RCANCEL_IMP = 
prove (`!x y z. ~(z = &0) /\ (x * z = y * z) ==> (x = y)`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN REWRITE_TAC[REAL_SUB_RZERO; GSYM REAL_SUB_RDISTRIB; REAL_ENTIRE] THEN CONV_TAC TAUT);;
let REAL_EQ_LCANCEL_IMP = 
prove (`!x y z. ~(z = &0) /\ (z * x = z * y) ==> (x = y)`,
ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN MATCH_ACCEPT_TAC REAL_EQ_RCANCEL_IMP);;
let REAL_LT_DIV = 
prove (`!x y. &0 < x /\ &0 < y ==> &0 < x / y`,
let REAL_LE_DIV = 
prove (`!x y. &0 <= x /\ &0 <= y ==> &0 <= x / y`,
let REAL_DIV_POW2 = 
prove (`!x m n. ~(x = &0) ==> (x pow m / x pow n = if n <= m then x pow (m - n) else inv(x pow (n - m)))`,
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[REAL_POW_SUB] THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_INV_INV] THEN AP_TERM_TAC THEN REWRITE_TAC[REAL_INV_DIV] THEN UNDISCH_TAC `~(n:num <= m)` THEN REWRITE_TAC[NOT_LE] THEN DISCH_THEN(MP_TAC o MATCH_MP LT_IMP_LE) THEN ASM_SIMP_TAC[REAL_POW_SUB]);;
let REAL_DIV_POW2_ALT = 
prove (`!x m n. ~(x = &0) ==> (x pow m / x pow n = if n < m then x pow (m - n) else inv(x pow (n - m)))`,
REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_INV_INV] THEN ONCE_REWRITE_TAC[REAL_INV_DIV] THEN ASM_SIMP_TAC[GSYM NOT_LE; REAL_DIV_POW2] THEN ASM_CASES_TAC `m <= n:num` THEN ASM_REWRITE_TAC[REAL_INV_INV]);;
let REAL_LT_POW2 = 
prove (`!n. &0 < &2 pow n`,
SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH]);;
let REAL_LE_POW2 = 
prove (`!n. &1 <= &2 pow n`,
GEN_TAC THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 pow 0` THEN SIMP_TAC[REAL_POW_MONO; LE_0; REAL_OF_NUM_LE; ARITH] THEN REWRITE_TAC[real_pow; REAL_LE_REFL]);;
let REAL_POW2_ABS = 
prove (`!x. abs(x) pow 2 = x pow 2`,
GEN_TAC THEN REWRITE_TAC[real_abs] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_POW_NEG; ARITH_EVEN]);;
let REAL_LE_SQUARE_ABS = 
prove (`!x y. abs(x) <= abs(y) <=> x pow 2 <= y pow 2`,
REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN MESON_TAC[REAL_POW_LE2; REAL_ABS_POS; NUM_EQ_CONV `2 = 0`; REAL_POW_LT2; REAL_NOT_LE]);;
let REAL_LT_SQUARE_ABS = 
prove (`!x y. abs(x) < abs(y) <=> x pow 2 < y pow 2`,
REWRITE_TAC[GSYM REAL_NOT_LE; REAL_LE_SQUARE_ABS]);;
let REAL_EQ_SQUARE_ABS = 
prove (`!x y. abs x = abs y <=> x pow 2 = y pow 2`,
REWRITE_TAC[GSYM REAL_LE_ANTISYM; REAL_LE_SQUARE_ABS]);;
let REAL_LE_POW_2 = 
prove (`!x. &0 <= x pow 2`,
REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]);;
let REAL_LT_POW_2 = 
prove (`!x. &0 < x pow 2 <=> ~(x = &0)`,
REWRITE_TAC[REAL_LE_POW_2; REAL_ARITH `&0 < x <=> &0 <= x /\ ~(x = &0)`] THEN REWRITE_TAC[REAL_POW_EQ_0; ARITH]);;
let REAL_SOS_EQ_0 = 
prove (`!x y. x pow 2 + y pow 2 = &0 <=> x = &0 /\ y = &0`,
REPEAT GEN_TAC THEN EQ_TAC THEN SIMP_TAC[REAL_POW_2; REAL_MUL_LZERO; REAL_ADD_LID] THEN DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH `x + y = &0 ==> &0 <= x /\ &0 <= y ==> x = &0 /\ y = &0`)) THEN REWRITE_TAC[REAL_LE_SQUARE; REAL_ENTIRE]);;
let REAL_POW_ZERO = 
prove (`!n. &0 pow n = if n = 0 then &1 else &0`,
INDUCT_TAC THEN REWRITE_TAC[real_pow; NOT_SUC; REAL_MUL_LZERO]);;
let REAL_POW_MONO_INV = 
prove (`!m n x. &0 <= x /\ x <= &1 /\ n <= m ==> x pow m <= x pow n`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `x = &0` THENL [ASM_REWRITE_TAC[REAL_POW_ZERO] THEN REPEAT(COND_CASES_TAC THEN REWRITE_TAC[REAL_POS; REAL_LE_REFL]) THEN UNDISCH_TAC `n:num <= m` THEN ASM_REWRITE_TAC[LE]; GEN_REWRITE_TAC BINOP_CONV [GSYM REAL_INV_INV] THEN MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[GSYM REAL_POW_INV] THEN CONJ_TAC THENL [MATCH_MP_TAC REAL_POW_LT THEN REWRITE_TAC[REAL_LT_INV_EQ]; MATCH_MP_TAC REAL_POW_MONO THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_INV_1_LE] THEN ASM_REWRITE_TAC[REAL_LT_LE]]);;
let REAL_POW_LE2_REV = 
prove (`!n x y. ~(n = 0) /\ &0 <= y /\ x pow n <= y pow n ==> x <= y`,
MESON_TAC[REAL_POW_LT2; REAL_NOT_LE]);;
let REAL_POW_LT2_REV = 
prove (`!n x y. &0 <= y /\ x pow n < y pow n ==> x < y`,
MESON_TAC[REAL_POW_LE2; REAL_NOT_LE]);;
let REAL_POW_EQ = 
prove (`!n x y. ~(n = 0) /\ &0 <= x /\ &0 <= y /\ x pow n = y pow n ==> x = y`,
REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN MESON_TAC[REAL_POW_LE2_REV]);;
let REAL_POW_EQ_ABS = 
prove (`!n x y. ~(n = 0) /\ x pow n = y pow n ==> abs x = abs y`,
REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_POW_EQ THEN EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[REAL_ABS_POS; GSYM REAL_ABS_POW]);;
let REAL_POW_EQ_1_IMP = 
prove (`!x n. ~(n = 0) /\ x pow n = &1 ==> abs(x) = &1`,
REPEAT STRIP_TAC THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_ABS_NUM] THEN MATCH_MP_TAC REAL_POW_EQ_ABS THEN EXISTS_TAC `n:num` THEN ASM_REWRITE_TAC[REAL_POW_ONE]);;
let REAL_POW_EQ_1 = 
prove (`!x n. x pow n = &1 <=> abs(x) = &1 /\ (x < &0 ==> EVEN(n)) \/ n = 0`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[real_pow] THEN ASM_CASES_TAC `abs(x) = &1` THENL [ALL_TAC; ASM_MESON_TAC[REAL_POW_EQ_1_IMP]] THEN ASM_REWRITE_TAC[] THEN FIRST_X_ASSUM(DISJ_CASES_THEN SUBST1_TAC o MATCH_MP (REAL_ARITH `abs x = a ==> x = a \/ x = --a`)) THEN ASM_REWRITE_TAC[REAL_POW_NEG; REAL_POW_ONE] THEN REPEAT COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC);;
let REAL_POW_LT2_ODD = 
prove (`!n x y. x < y /\ ODD n ==> x pow n < y pow n`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[ARITH] THEN STRIP_TAC THEN DISJ_CASES_TAC(SPEC `y:real` REAL_LE_NEGTOTAL) THENL [DISJ_CASES_TAC(REAL_ARITH `&0 <= x \/ &0 < --x`) THEN ASM_SIMP_TAC[REAL_POW_LT2] THEN SUBGOAL_THEN `&0 < --x pow n /\ &0 <= y pow n` MP_TAC THENL [ASM_SIMP_TAC[REAL_POW_LE; REAL_POW_LT]; ASM_REWRITE_TAC[REAL_POW_NEG; GSYM NOT_ODD] THEN REAL_ARITH_TAC]; SUBGOAL_THEN `--y pow n < --x pow n` MP_TAC THENL [MATCH_MP_TAC REAL_POW_LT2 THEN ASM_REWRITE_TAC[]; ASM_REWRITE_TAC[REAL_POW_NEG; GSYM NOT_ODD]] THEN REPEAT(POP_ASSUM MP_TAC) THEN REAL_ARITH_TAC]);;
let REAL_POW_LE2_ODD = 
prove (`!n x y. x <= y /\ ODD n ==> x pow n <= y pow n`,
REWRITE_TAC[REAL_LE_LT] THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC[REAL_POW_LT2_ODD]);;
let REAL_POW_LT2_ODD_EQ = 
prove (`!n x y. ODD n ==> (x pow n < y pow n <=> x < y)`,
let REAL_POW_LE2_ODD_EQ = 
prove (`!n x y. ODD n ==> (x pow n <= y pow n <=> x <= y)`,
let REAL_POW_EQ_ODD_EQ = 
prove (`!n x y. ODD n ==> (x pow n = y pow n <=> x = y)`,
SIMP_TAC[GSYM REAL_LE_ANTISYM; REAL_POW_LE2_ODD_EQ]);;
let REAL_POW_EQ_ODD = 
prove (`!n x y. ODD n /\ x pow n = y pow n ==> x = y`,
MESON_TAC[REAL_POW_EQ_ODD_EQ]);;
let REAL_POW_EQ_EQ = 
prove (`!n x y. x pow n = y pow n <=> if EVEN n then n = 0 \/ abs x = abs y else x = y`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[real_pow; ARITH] THEN COND_CASES_TAC THEN ASM_SIMP_TAC[REAL_POW_EQ_ODD_EQ; GSYM NOT_EVEN] THEN EQ_TAC THENL [ASM_MESON_TAC[REAL_POW_EQ_ABS]; ALL_TAC] THEN REWRITE_TAC[REAL_EQ_SQUARE_ABS] THEN DISCH_TAC THEN FIRST_X_ASSUM(X_CHOOSE_THEN `m:num` SUBST1_TAC o REWRITE_RULE[EVEN_EXISTS]) THEN ASM_REWRITE_TAC[GSYM REAL_POW_POW]);;
(* ------------------------------------------------------------------------- *) (* Some basic forms of the Archimedian property. *) (* ------------------------------------------------------------------------- *)
let REAL_ARCH_SIMPLE = 
prove (`!x. ?n. x <= &n`,
let lemma = prove(`(!x. (?n. x = &n) ==> P x) <=> !n. P(&n)`,MESON_TAC[]) in
  MP_TAC(SPEC `\y. ?n. y = &n` REAL_COMPLETE) THEN REWRITE_TAC[lemma] THEN
  MESON_TAC[REAL_LE_SUB_LADD; REAL_OF_NUM_ADD; REAL_LE_TOTAL;
            REAL_ARITH `~(M <= M - &1)`]);;
let REAL_ARCH_LT = 
prove (`!x. ?n. x < &n`,
MESON_TAC[REAL_ARCH_SIMPLE; REAL_OF_NUM_ADD; REAL_ARITH `x <= n ==> x < n + &1`]);;
let REAL_ARCH = 
prove (`!x. &0 < x ==> !y. ?n. y < &n * x`,
(* ------------------------------------------------------------------------- *) (* The sign of a real number, as a real number. *) (* ------------------------------------------------------------------------- *)
let real_sgn = new_definition
 `(real_sgn:real->real) x =
        if &0 < x then &1 else if x < &0 then -- &1 else &0`;;
let REAL_SGN_0 = 
prove (`real_sgn(&0) = &0`,
REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
let REAL_SGN_NEG = 
prove (`!x. real_sgn(--x) = --(real_sgn x)`,
REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
let REAL_SGN_ABS = 
prove (`!x. real_sgn(x) * abs(x) = x`,
REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
let REAL_EQ_SGN_ABS = 
prove (`!x y:real. x = y <=> real_sgn x = real_sgn y /\ abs x = abs y`,
MESON_TAC[REAL_SGN_ABS]);;
let REAL_ABS_SGN = 
prove (`!x. abs(real_sgn x) = real_sgn(abs x)`,
REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
let REAL_SGN = 
prove (`!x. real_sgn x = x / abs x`,
GEN_TAC THEN ASM_CASES_TAC `x = &0` THENL [ASM_REWRITE_TAC[real_div; REAL_MUL_LZERO; REAL_SGN_0]; GEN_REWRITE_TAC (RAND_CONV o LAND_CONV) [GSYM REAL_SGN_ABS] THEN ASM_SIMP_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_ABS_ZERO; REAL_MUL_RINV; REAL_MUL_RID]]);;
let REAL_SGN_MUL = 
prove (`!x y. real_sgn(x * y) = real_sgn(x) * real_sgn(y)`,
REWRITE_TAC[REAL_SGN; REAL_ABS_MUL; real_div; REAL_INV_MUL] THEN REAL_ARITH_TAC);;
let REAL_SGN_INV = 
prove (`!x. real_sgn(inv x) = real_sgn x`,
REWRITE_TAC[real_sgn; REAL_LT_INV_EQ; GSYM REAL_INV_NEG; REAL_ARITH `x < &0 <=> &0 < --x`]);;
let REAL_SGN_DIV = 
prove (`!x y. real_sgn(x / y) = real_sgn(x) / real_sgn(y)`,
REWRITE_TAC[REAL_SGN; REAL_ABS_DIV] THEN REWRITE_TAC[real_div; REAL_INV_MUL; REAL_INV_INV] THEN REAL_ARITH_TAC);;
let REAL_SGN_EQ = 
prove (`(!x. real_sgn x = &0 <=> x = &0) /\ (!x. real_sgn x = &1 <=> x > &0) /\ (!x. real_sgn x = -- &1 <=> x < &0)`,
REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
let REAL_SGN_CASES = 
prove (`!x. real_sgn x = &0 \/ real_sgn x = &1 \/ real_sgn x = -- &1`,
REWRITE_TAC[real_sgn] THEN MESON_TAC[]);;
let REAL_SGN_INEQS = 
prove (`(!x. &0 <= real_sgn x <=> &0 <= x) /\ (!x. &0 < real_sgn x <=> &0 < x) /\ (!x. &0 >= real_sgn x <=> &0 >= x) /\ (!x. &0 > real_sgn x <=> &0 > x) /\ (!x. &0 = real_sgn x <=> &0 = x) /\ (!x. real_sgn x <= &0 <=> x <= &0) /\ (!x. real_sgn x < &0 <=> x < &0) /\ (!x. real_sgn x >= &0 <=> x >= &0) /\ (!x. real_sgn x > &0 <=> x > &0) /\ (!x. real_sgn x = &0 <=> x = &0)`,
REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
let REAL_SGN_POW = 
prove (`!x n. real_sgn(x pow n) = real_sgn(x) pow n`,
GEN_TAC THEN INDUCT_TAC THEN ASM_REWRITE_TAC[REAL_SGN_MUL; real_pow] THEN REWRITE_TAC[real_sgn; REAL_LT_01]);;
let REAL_SGN_POW_2 = 
prove (`!x. real_sgn(x pow 2) = real_sgn(abs x)`,
REWRITE_TAC[real_sgn] THEN SIMP_TAC[GSYM REAL_NOT_LE; REAL_ABS_POS; REAL_LE_POW_2; REAL_ARITH `&0 <= x ==> (x <= &0 <=> x = &0)`] THEN REWRITE_TAC[REAL_POW_EQ_0; REAL_ABS_ZERO; ARITH]);;
let REAL_SGN_REAL_SGN = 
prove (`!x. real_sgn(real_sgn x) = real_sgn x`,
REWRITE_TAC[real_sgn] THEN REAL_ARITH_TAC);;
let REAL_INV_SGN = 
prove (`!x. real_inv(real_sgn x) = real_sgn x`,
GEN_TAC THEN REWRITE_TAC[real_sgn] THEN REPEAT COND_CASES_TAC THEN REWRITE_TAC[REAL_INV_0; REAL_INV_1; REAL_INV_NEG]);;
(* ------------------------------------------------------------------------- *) (* Useful "without loss of generality" lemmas. *) (* ------------------------------------------------------------------------- *)
let REAL_WLOG_LE = 
prove (`(!x y. P x y <=> P y x) /\ (!x y. x <= y ==> P x y) ==> !x y. P x y`,
MESON_TAC[REAL_LE_TOTAL]);;
let REAL_WLOG_LT = 
prove (`(!x. P x x) /\ (!x y. P x y <=> P y x) /\ (!x y. x < y ==> P x y) ==> !x y. P x y`,
MESON_TAC[REAL_LT_TOTAL]);;