|
This proof proves the theorem
 a: . n: .
p,q:. Div(a;n;p)   Div(a;n;q) p = q
where Div(a;n;q) == n * q  a < n * (q + 1)
The following lemmas are used in this proof:
- lt_transitivity_2
- i,j,k:
 . i j j < k i < k
- mul_cancel_in_lt
- a,b:. n:. n * a < n * b a < b
Please do the following and record your answers:
- Translate this proof into English.
- Was there any part of this proof that you found difficult to translate? If
so, why?
- Do you think that this theorem was proved in a natural or intuitive
manner or not? If so, why?
|
|
