a:
, n:
. (a rem n) = a-(a 
n)
na,b,n:. a+n = b+n 
a = ba:, n:. a = (a n)n+(a rem n)| Theorem | Name |
|
Thm* a:, n:. (a rem n) = a-(a n)n | [rem_to_div] |
| cites | |
|
Thm* a,b,n:. a+n = b+n a = b | [add_cancel_in_eq] |
|
Thm* a:, n:. a = (a n)n+(a rem n) | [div_rem_sum] |