|
This proof proves the theorem
 a: . n: . a < n   a  n = 0
The following definition is used in this proof:
- div_nrel (natural number division)
- Div(a;n;q) == n * q
 a < n * (q + 1)
The following lemmas are used in this proof:
- div_fun_sat_div_nrel
- a:. n:. Div(a;n;a n)
- div_unique
- a:. n:. p,q:. Div(a;n;p) Div(a;n;q) p=q
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?
|
|
