1pub const COMMON_FACTS: &str = r#"
2know:
3 + $in fn(a, b R) R
4 - $in fn(a, b R) R
5 * $in fn(a, b R) R
6 / $in fn(a R, b R: b != 0) R
7 % $in fn(a Z, b Z: b != 0) Z
8 ^ $in fn(a, b R: a $in R_pos or a = 0 and b $in R_pos or a $in R_nz and b $in Z or b $in N_pos) R
9
10know:
11 forall a, b R:
12 =>:
13 a = 0 and b = 0
14 <=>:
15 a ^ 2 + b ^ 2 = 0
16
17
18 forall a, b R:
19 a <= max(a, b)
20 b <= max(a, b)
21
22 forall a, b R:
23 min(a, b) <= a
24 min(a, b) <= b
25
26 forall a, b R:
27 max(a, b) = max(b, a)
28 min(a, b) = min(b, a)
29
30 forall a,b R:
31 a*b!=0
32 =>:
33 a!=0 and b!=0
34
35 forall a R_pos, b R_nz:
36 0 < a ^ b
37 a = (a^b)^(1/b)
38
39 forall a R_pos, b R_nz:
40 a = (a^(1/b))^b
41
42 forall a R_pos, b R, c R:
43 (a^b)^c = a^(b*c)
44
45 forall a R_pos, b R, c R:
46 a^(b+c) = a^b * a^c
47
48 forall a R_pos, b R:
49 a * a^b = a^(b+1)
50 a^b * a = a^(b+1)
51
52 forall a R_nz, b Z:
53 a * a^b = a^(b+1)
54 a^b * a = a^(b+1)
55
56 forall a R_pos, b R_pos:
57 a != 1
58 =>:
59 a ^ (log(a, b)) = b
60
61 forall a, b, c Z:
62 c != 0
63 =>:
64 (a + b) % c = ((a % c) + (b % c)) % c
65 (a - b) % c = ((a % c) - (b % c)) % c
66
67 forall n Z, k N_pos:
68 (-n) % k = (k - (n % k)) % k
69
70 forall n Z, m Z:
71 n <= m or n >= m + 1
72 n < m or n >= m
73 n >= m or n <= m - 1
74 n > m or n <= m
75
76 forall n Z, m N_pos, k N_pos:
77 n^m % k = ((n % k)^m) % k
78
79 forall a, b N:
80 a <= b
81 b != 0
82 =>:
83 a % b = b
84
85prop archimedean_property(e R_pos):
86 exist n N_pos st {1/n < e}
87
88know:
89 forall e R_pos:
90 $archimedean_property(e)
91 exist n N_pos st {1/n < e}
92
93know:
94 forall s set:
95 seq(s) = fn(x N_pos) s
96
97 forall s set, n N_pos:
98 finite_seq(s, n) = fn(x N_pos: x <= n) s
99
100 forall s set, m N_pos, n N_pos:
101 matrix(s, m, n) = fn(x, y N_pos: x <= m, y <= n) s
102
103 forall a Z, m N_pos:
104 (a % m) $in N
105 (a % m) < m
106
107 forall a Z, m N_pos, k N:
108 a % m = k
109 =>:
110 exist r Z st {a = m * r + k}
111
112 forall a Z, m N_pos, k N:
113 k < m
114 exist r Z st {a = m * r + k}
115 =>:
116 a % m = k
117
118 forall a Z, m N_pos:
119 exist r Z st {a = m * r}
120 =>:
121 a % m = 0
122
123 forall a Z, m N_pos:
124 exist r Z st {a = r * m}
125 =>:
126 a % m = 0
127
128 forall a Z, m N_pos:
129 a % m = 0
130 =>:
131 exist r Z st {a = m * r}
132
133 forall a Z, m N_pos:
134 a % m = 0
135 =>:
136 exist r Z st {a = r * m}
137
138 forall a Z, m N_pos, k N:
139 k < m
140 exist r Z st {a = r * m + k}
141 =>:
142 a % m = k
143
144 forall a N, m N_pos, k N:
145 a % m = k
146 =>:
147 exist r N st {a = m * r + k}
148
149 forall a N, m N_pos, k N:
150 k < m
151 exist r N st {a = m * r + k}
152 =>:
153 a % m = k
154
155 forall a N, m N_pos:
156 exist r N st {a = m * r}
157 =>:
158 a % m = 0
159
160 forall a N, m N_pos:
161 exist r N st {a = r * m}
162 =>:
163 a % m = 0
164
165 forall a N, m N_pos:
166 a % m = 0
167 =>:
168 exist r N st {a = m * r}
169
170 forall a N, m N_pos:
171 a % m = 0
172 =>:
173 exist r N st {a = r * m}
174
175 forall a N, m N_pos, k N:
176 k < m
177 exist r N st {a = r * m + k}
178 =>:
179 a % m = k
180
181 forall a finite_set:
182 count(a) = 0
183 =>:
184 not $is_nonempty_set(a)
185 a = {}
186
187 forall a, b N_pos:
188 a % b = 0
189 =>:
190 b <= a
191
192 forall a Q:
193 exist p Z, q N_pos st {a = p / q}
194
195 forall a Q:
196 a >= 0
197 =>:
198 exist p N, q N_pos st {a = p / q}
199
200prop even_power_abs_bound(x, y R, k N_pos):
201 abs(x) <= abs(y)
202
203prop even_power_bound_by_nonnegative_rhs(x, y R, k N_pos):
204 -y <= x
205 x <= y
206
207prop even_power_bound_by_nonpositive_rhs(x, y R, k N_pos):
208 y <= x
209 x <= -y
210
211know:
212 forall x, y R, k N_pos:
213 k % 2 = 0
214 x^k <= y^k
215 =>:
216 $even_power_abs_bound(x, y, k)
217
218 forall x, y R, k N_pos:
219 k % 2 = 0
220 x^k <= y^k
221 y >= 0
222 =>:
223 $even_power_bound_by_nonnegative_rhs(x, y, k)
224
225 forall x, y R, k N_pos:
226 k % 2 = 0
227 x^k <= y^k
228 y <= 0
229 =>:
230 $even_power_bound_by_nonpositive_rhs(x, y, k)
231
232"#;