1 REAL_ARITH `!x y:real. (abs(x) - abs(y)) <= abs(x - y)`;;
5 (a pow 2 - D * b pow 2) * (a' pow 2 - D * b' pow 2) =
6 (a * a' + D * b * b') pow 2 - D * (a * b' + a' * b) pow 2`;;
9 `!x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11:real.
19 ==> x1 = x10 /\ x2 = x11`;;
21 REAL_ARITH `!x y:real. x < y ==> x < (x + y) / &2 /\ (x + y) / &2 < y`;;
24 `((x1 pow 2 + x2 pow 2 + x3 pow 2 + x4 pow 2) pow 2) =
25 ((&1 / &6) * ((x1 + x2) pow 4 + (x1 + x3) pow 4 + (x1 + x4) pow 4 +
26 (x2 + x3) pow 4 + (x2 + x4) pow 4 + (x3 + x4) pow 4) +
27 (&1 / &6) * ((x1 - x2) pow 4 + (x1 - x3) pow 4 + (x1 - x4) pow 4 +
28 (x2 - x3) pow 4 + (x2 - x4) pow 4 + (x3 - x4) pow 4))`;;
30 ARITH_RULE `x < 2 ==> 2 * x + 1 < 4`;;
33 ARITH_RULE `~(2 * m + 1 = 2 * n)`;;
36 ARITH_RULE `x < 2 EXP 30 ==> (429496730 * x) DIV (2 EXP 32) = x DIV 10`;;
39 ARITH_RULE `x <= 2 EXP 30 ==> (429496730 * x) DIV (2 EXP 32) = x DIV 10`;;
43 ARITH_RULE `1 <= x /\ 1 <= y ==> 1 <= x * y`;;
47 REAL_ARITH `!x y:real. x = y ==> x * y = y pow 2`;;
54 ==> s * (s - b) * (s - c) + s * (s - c) * (s - a) +
55 s * (s - a) * (s - b) - (s - a) * (s - b) * (s - c) =
58 REAL_RING `a pow 2 = &2 /\ x pow 2 + a * x + &1 = &0 ==> x pow 4 + &1 = &0`;;
61 `(a * x pow 2 + b * x + c = &0) /\
62 (a * y pow 2 + b * y + c = &0) /\
64 ==> (a * x * y = c) /\ (a * (x + y) + b = &0)`;;
67 `p = (&3 * a1 - a2 pow 2) / &3 /\
68 q = (&9 * a1 * a2 - &27 * a0 - &2 * a2 pow 3) / &27 /\
70 x * w = w pow 2 - p / &3
71 ==> (z pow 3 + a2 * z pow 2 + a1 * z + a0 = &0 <=>
72 if p = &0 then x pow 3 = q
73 else (w pow 3) pow 2 - q * (w pow 3) - p pow 3 / &27 = &0)`;;
75 REAL_FIELD `&0 < x ==> &1 / x - &1 / (&1 + x) = &1 / (x * (&1 + x))`;;
78 `s pow 2 = b pow 2 - &4 * a * c
79 ==> (a * x pow 2 + b * x + c = &0 <=>
82 if c = &0 then T else F
84 else x = (--b + s) / (&2 * a) \/ x = (--b + --s) / (&2 * a))`;;
86 (**** This needs an external SDP solver to assist with proof
88 needs "Examples/sos.ml";;
90 SOS_RULE `1 <= x /\ 1 <= y ==> 1 <= x * y`;;
94 &0 <= a1 /\ &0 <= a2 /\ &0 <= a3 /\ &0 <= a4
96 ((a1 + a2) / &2) pow 2 +
97 ((a1 + a2 + a3) / &3) pow 2 +
98 ((a1 + a2 + a3 + a4) / &4) pow 2
99 <= &4 * (a1 pow 2 + a2 pow 2 + a3 pow 2 + a4 pow 2)`;;
103 a >= &0 /\ b >= &0 /\ c >= &0
104 ==> &3 / &2 * (b + c) * (a + c) * (a + b) <=
105 a * (a + c) * (a + b) +
106 b * (b + c) * (a + b) +
107 c * (b + c) * (a + c)`;;
109 SOS_CONV `&2 * x pow 4 + &2 * x pow 3 * y - x pow 2 * y pow 2 + &5 * y pow 4`;;
112 `x pow 4 + &2 * x pow 2 * z + x pow 2 - &2 * x * y * z +
113 &2 * y pow 2 * z pow 2 + &2 * y * z pow 2 + &2 * z pow 2 - &2 * x +
114 &2 * y * z + &1 >= &0`;;
118 needs "Examples/cooper.ml";;
120 COOPER_RULE `ODD n ==> 2 * n DIV 2 < n`;;
122 COOPER_RULE `!n. n >= 8 ==> ?a b. n = 3 * a + 5 * b`;;
124 needs "Rqe/make.ml";;
126 REAL_QELIM_CONV `!x. &0 <= x ==> ?y. y pow 2 = x`;;