q 
a < n(q+1)
Thm* 
a:
, n:
, q:. Div(a;n;q) 
Prop
j < k == ij & j < k
B == 
B < A
Thm* i,j:
. ij Prop
A == A 
False
Thm* A:Prop. (A) Prop
| div_nrel |
Def Div(a;n;q) == nq a < n(q+1)
Thm* |
| lelt |
Def i j < k == ij & j < k
|
| le |
Def AB == B < A
Thm* |
| not |
Def A == A False
Thm* |
About:
 |  |  |  |  |  |
 |  |  |  |  |  |