|
This proof proves the theorem
 a,b: . a * b > 0    (a > 0  b > 0)  (a < 0 b < 0)
The following lemmas are used in this proof:
- int_trichot
- i,j:. i < j i = j i > j
- mul_bounds_1b
- a,b:
  . 0 < a * b
- 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?
|
|
