a:
, b:
. ((-a) rem b) = -(a rem b)k:
, r1,r2:k, q1,q2:. q1
k+r1 = q2k+r2 
q1 = q2 & r1 = r2a:, b:. (a rem -b) = (a rem b)| Rank | Theorem | Name |
| 4 | a:, b:. ((-a) rem b) = -(a rem b) | [rem_antisym] |
| cites the following: | ||
| 2 | k:, r1,r2:k, q1,q2:. q1k+r1 = q2k+r2 q1 = q2 & r1 = r2 | [division1_sfa] |
| 3 | a:, b:. (a rem -b) = (a rem b) | [rem_sym] |