a:
, n:
. n | a 
(a 
n)
n = aa:, b:. b | a (a rem b) = 0a,b,n:. a = b a+n = b+na:, n:. a = (a n)n+(a rem n)| Rank | Theorem | Name |
| 7 | a:, n:. n | a (a n)n = a | [divides_iff_div_exact] |
| cites the following: | ||
| 6 | a:, b:. b | a (a rem b) = 0 | [divides_iff_rem_zero] |
| 0 | a,b,n:. a = b a+n = b+n | [add_mono_wrt_eq] |
| 0 | a:, n:. a = (a n)n+(a rem n) | [div_rem_sum] |