| 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:. ab a+nb+n | [add_mono_wrt_le] |
| 0 | Thm* i,j,k:. i < j  jk i < k | [lt_transitivity_1] |
| 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] |