|
This proof proves the theorem
 a: . n: . a  n   a  n = (a - n) n + 1
The following lemmas are used in this proof:
- add_cancel_in_le
- a,b,n:
 . a + n  b + n a b
- add_cancel_in_lt
- a,b,n:. a + n < b + n a < b
- add_mono_wrt_le_rw
- a,b,n:. {a b
 a + n b + n}
- div_elim
- a:. n:.
 q:. Div(a;n;q)  a n = q
- 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?
|
|
