a:
, n:
. a
n 
(a rem n) = ((a-n) rem n)a:, n:. an (a 
n) = ((a-n) n)+1a:{...0}, n:{...-1}. 0(a rem n) & (a rem n) > na:{...0}, n:. 0(a rem n) & (a rem n) > -ni1,i2,j1,j2:
. i1
j1 i2j2 i1-i2j1-j2i,j:. ij -i-jj == ji
is mentioned by
|
Thm* a:, n:. an (a rem n) = ((a-n) rem n) | [rem_rec_case] |
|
Thm* a:, n:. an (a n) = ((a-n) n)+1 | [div_rec_case] |
|
Thm* a:{...0}, n:{...-1}. 0(a rem n) & (a rem n) > n | [rem_bounds_3] |
|
Thm* a:{...0}, n:. 0(a rem n) & (a rem n) > -n | [rem_bounds_2] |
|
Thm* i1,i2,j1,j2:. i1j1 i2j2 i1-i2j1-j2 | [sub_functionality_wrt_le] |
|
Thm* i,j:. ij -i-j | [minus_functionality_wrt_le] |
Try larger context: StandardLIB