| Rank | Theorem | Name |
| 6 | Thm*  a: , b:  . b | a   (a rem b) = 0 | [divides_iff_rem_zero] |
| cites the following: |
| 4 | Thm* a: , n: .  q:. Div(a;n;q) & (a  n) = q | [div_elim] |
| 1 | Thm* a,b:, n:. n a<nb  a<b | [mul_cancel_in_lt] |
| 2 | Thm* a,b:, n:. na nb ab | [mul_cancel_in_le] |
| 4 | Thm* a:, n:{...-1}. (a rem n) = (a rem -n) | [rem_4_to_1] |
| 5 | Thm* a:{...0}, n:. (a rem n) = -((-a) rem n) | [rem_2_to_1] |
| 5 | Thm* a:{...0}, n:{...-1}. (a rem n) = -((-a) rem -n) | [rem_3_to_1] |
| 1 | Thm* a,b:. a | b a | -b | [divides_invar_2] |
| 0 | Thm* a,b:. a | b -a | b | [divides_invar_1] |
| 1 | Thm* a:, n:. (a rem n) = a-(a n)n | [rem_to_div] |
| 0 | Thm* a,b,n:. a = b a+n = b+n | [add_mono_wrt_eq] |