pub const COMMON_FACTS: &str = r#"
know:
forall a, b R:
=>:
a = 0 and b = 0
<=>:
a ^ 2 + b ^ 2 = 0
forall a R:
a >= 0
=>:
abs(a) = a
forall a R:
a <= 0
=>:
abs(a) = -a
forall a R:
abs(a) >= 0
abs(a) = a or abs(a) = -a
forall a R:
abs(a) = 0
=>:
a = 0
forall a, b R:
a <= max(a, b)
b <= max(a, b)
forall a, b R:
min(a, b) <= a
min(a, b) <= b
forall a, b R:
max(a, b) = max(b, a)
min(a, b) = min(b, a)
forall a,b R:
a*b!=0
=>:
a!=0 and b!=0
forall a R_pos, b R_nz:
0 < a ^ b
a = (a^b)^(1/b)
forall a R_pos, b R_nz:
a = (a^(1/b))^b
forall a R_pos, b R, c R:
(a^b)^c = a^(b*c)
forall a R_pos, b R, c R:
a^(b+c) = a^b * a^c
forall a R_pos, b R_pos:
a != 1
=>:
a ^ (log(a, b)) = b
forall a, b, c Z:
c != 0
=>:
(a + b) % c = ((a % c) + (b % c)) % c
(a - b) % c = ((a % c) - (b % c)) % c
forall n Z, k N_pos:
(-n) % k = (k - (n % k)) % k
forall n Z, m N_pos, k N_pos:
n^m % k = ((n % k)^m) % k
forall x R:
0 <= abs(x)
abs(x) = x or abs(x) = -x
forall x, y R:
abs(x * y) = abs(x) * abs(y)
forall a, b N:
a <= b
b != 0
=>:
a % b = b
prop archimedean_property(e R_pos):
exist n N_pos st {1/n < e}
know:
forall e R_pos:
$archimedean_property(e)
exist n N_pos st {1/n < e}
"#;