a,b:
, n:
. ((a+b
n) rem n) = (a rem n)i,j:. ij 
k:, r1,r2:k, q1,q2:
. q1k+r1 = q2k+r2 
q1 = q2 & r1 = r2| Rank | Theorem | Name |
| 3 | a,b:, n:. ((a+bn) rem n) = (a rem n) | [rem_invariant] |
| cites the following: | ||
| 2 | i,j:. ij | [multiply_nat_wf] |
| 2 | k:, r1,r2:k, q1,q2:. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2 | [division1_sfa] |