| Who Cites rem nrel? |
|
rem_nrel | Def Rem(a;n;r) == q:. Div(a;n;q) & qn+r = a |
| | Thm* a:, n:, r:. Rem(a;n;r) Prop |
|
div_nrel | Def Div(a;n;q) == nq a < n(q+1) |
| | Thm* a:, n:, q:. Div(a;n;q) Prop |
|
nat | Def == {i:| 0i } |
| | Thm* Type |
|
lelt | Def i j < k == ij & j<k |
|
le | Def AB == B<A |
| | Thm* i,j:. (ij) Prop |
|
not | Def A == A False |
| | Thm* A:Prop. (A) Prop |