a
a rem n ; ((-a) rem n)=0 0 else n-((-a) rem n) fi
a:
, n:
. (a mod n) 
j == if i=j true ; false fii,j:. (i=j) 
B == 
B<Ai,j:. (ij) Propj == j<ii,j:. (ij) == {i:| 0<i } Type| Some definitions of interest. | |
| modulus | a a rem n ; ((-a) rem n)=0 0 else n-((-a) rem n) fi |
| a:, n:. (a mod n) | |
| eq_int | j == if i=j true ; false fi |
| i,j:. (i=j) | |
| le | B == B<A |
| i,j:. (ij) Prop | |
| le_int | j == j<i |
| i,j:. (ij) | |
| nat_plus | == {i:| 0<i } |
| Type |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |
 |