a:
, n:
, k:. k
(a 
n) 
k
naa,b:
, n:. ab 
nanbk:, r1,r2:k, q1,q2:. q1k+r1q2k+r2 q1q2| Rank | Theorem | Name |
| 3 | a:, n:, k:. k(a n) kna | [div_lbound_1] |
| cites the following: | ||
| 0 | a,b:, n:. ab nanb | [mul_preserves_le] |
| 2 | k:, r1,r2:k, q1,q2:. q1k+r1q2k+r2 q1q2 | [division_mono1_sfa] |