| | Some definitions of interest. |
|
| prime | Def prime(a) ==  a = 0 & (a ~ 1) & ( b,c: . (a | (b c))   (a | b)  (a | c)) |
| | | Thm* a:. prime(a)  Prop |
|
| assoced | Def a ~ b == (a | b) & (b | a) |
| | | Thm* a,b:. (a ~ b) Prop |
|
| div_floor | Def a   n == if 0  a a n ;((-a) rem n)=0-((-a) n) else -((-a) n)+-1 fi |
| | | Thm* a:, n:  . (a n) |
|
| divides | Def b | a ==  c:. a = bc |
| | | Thm* a,b:. (a | b) Prop |
|
| int_nzero | Def   == {i:| i  0 } |
| | | Thm* Type |
|
| nat | Def == {i:| 0i } |
| | | Thm* Type |
|
| le | Def AB == B < A |
| | | Thm* i,j:. (ij) Prop |
|
| modulus | Def a mod n == if 0aa rem n ;((-a) rem n)=00 else n-((-a) rem n) fi |
| | | Thm* a:, n:. (a mod n) |
|
| not | Def A == A False |
| | | Thm* A:Prop. (A) Prop |
