| Rank | Theorem | Name |
| 4 |
Thm*  a: , b:{...-1}. (a  b) = -(a (-b)) | [div_4_to_1] |
| cites |
| 0 |
Thm* a:, n:{...-1}. 0 (a rem n) & (a rem n) < -n | [rem_bounds_4] |
| 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:. ab a+nb+n | [add_mono_wrt_le] |
| 0 | Thm* i,j,k:. ij  j < k i < k | [lt_transitivity_2] |
| 2 |
Thm* a,b:, n:. na < nb a < b | [mul_cancel_in_lt] |
| 0 | Thm* i,j:. i > j -i < -j | [minus_functionality_wrt_lt] |