1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
// Order closure on R for +, -, *, / using only <= and < in conclusions (see also tmp.lit).
pub const BUILTIN_ENV_CODE_FOR_REAL_ARITHMETIC_ORDER_CLOSURE: &str = r#"
know:
forall a, b, x R:
0 <= x
a <= b
=>:
a * x <= b * x
x * a <= x * b
forall a, b, x R:
x <= 0
a <= b
=>:
b * x <= a * x
x * b <= x * a
forall a, b, c, d R:
a <= b
c <= d
=>:
a + c <= b + d
forall a, b, c, d R:
a <= b
c <= d
=>:
a - d <= b - c
forall a, b, c, d R:
a < b
c < d
=>:
a + c < b + d
forall a, b, c, d R:
a <= b
c < d
=>:
a + c < b + d
forall a, b, c, d R:
a < b
c <= d
=>:
a + c < b + d
forall a, b, x R:
0 < x
a < b
=>:
a * x < b * x
x * a < x * b
forall a, b, x R:
0 < x
a <= b
=>:
a * x <= b * x
x * a <= x * b
forall a, b, x R:
x < 0
a < b
=>:
b * x < a * x
forall a, b, x R:
x < 0
a <= b
=>:
b * x <= a * x
forall a, b, c R:
0 < c
a <= b
=>:
a / c <= b / c
forall a, b, c R:
0 < c
a < b
=>:
a / c < b / c
forall a, b, c R:
c < 0
a <= b
=>:
b / c <= a / c
forall a, b, c R:
c < 0
a < b
=>:
b / c < a / c
forall a, b R:
a <= b
=>:
a - b <= 0
forall a, b R:
a - b <= 0
=>:
a <= b
forall a, b R:
a < b
=>:
a - b < 0
forall a, b R:
a - b < 0
=>:
a < b
"#;