Rank | Theorem | Name |
4 |
Thm* a:{...0}, b:{...-1}. (a b) = ((-a) (-b)) | [div_3_to_1] |
cites |
0 |
Thm* a:{...0}, n:{...-1}. 0 (a rem n) & (a rem n) > n | [rem_bounds_3] |
0 |
Thm* a: , n: . 0 (a rem n) & (a rem n) < n | [rem_bounds_1] |
0 |
Thm* a: , n:  . a = (a n) n+(a rem n) | [div_rem_sum] |
1 |
Thm* a,b,n: . a = b  a+n = b+n | [add_mono_wrt_eq] |
3 |
Thm* a,b,n: . a < b  a+n < b+n | [add_mono_wrt_lt] |
2 |
Thm* a,b,n: . a b  a+n b+n | [add_mono_wrt_le] |
0 | Thm* i,j,k: . i < j  j k  i < k | [lt_transitivity_1] |
2 |
Thm* a,b: , n: . n a < n b  a < b | [mul_cancel_in_lt] |
0 | Thm* i,j: . i > j  -i < -j | [minus_functionality_wrt_lt] |