5 |
5 |
6 Common factor cancellation |
6 Common factor cancellation |
7 *) |
7 *) |
8 |
8 |
9 val real_diff_minus_eq = thm"real_diff_minus_eq"; |
9 val real_diff_minus_eq = thm"real_diff_minus_eq"; |
10 val real_0_divide = thm"real_0_divide"; |
|
11 val real_0_less_inverse_iff = thm"real_0_less_inverse_iff"; |
|
12 val real_inverse_less_0_iff = thm"real_inverse_less_0_iff"; |
|
13 val real_0_le_inverse_iff = thm"real_0_le_inverse_iff"; |
|
14 val real_inverse_le_0_iff = thm"real_inverse_le_0_iff"; |
|
15 val real_inverse_eq_divide = thm"real_inverse_eq_divide"; |
10 val real_inverse_eq_divide = thm"real_inverse_eq_divide"; |
16 val real_0_less_divide_iff = thm"real_0_less_divide_iff"; |
|
17 val real_divide_less_0_iff = thm"real_divide_less_0_iff"; |
|
18 val real_0_le_divide_iff = thm"real_0_le_divide_iff"; |
11 val real_0_le_divide_iff = thm"real_0_le_divide_iff"; |
19 val real_divide_le_0_iff = thm"real_divide_le_0_iff"; |
|
20 val real_inverse_zero_iff = thm"real_inverse_zero_iff"; |
|
21 val real_divide_eq_0_iff = thm"real_divide_eq_0_iff"; |
|
22 val real_divide_self_eq = thm"real_divide_self_eq"; |
|
23 val real_minus_less_minus = thm"real_minus_less_minus"; |
|
24 val real_mult_less_mono1_neg = thm"real_mult_less_mono1_neg"; |
|
25 val real_mult_less_mono2_neg = thm"real_mult_less_mono2_neg"; |
|
26 val real_mult_le_mono1_neg = thm"real_mult_le_mono1_neg"; |
|
27 val real_mult_le_mono2_neg = thm"real_mult_le_mono2_neg"; |
|
28 val real_mult_less_cancel2 = thm"real_mult_less_cancel2"; |
12 val real_mult_less_cancel2 = thm"real_mult_less_cancel2"; |
29 val real_mult_le_cancel2 = thm"real_mult_le_cancel2"; |
13 val real_mult_le_cancel2 = thm"real_mult_le_cancel2"; |
30 val real_mult_less_cancel1 = thm"real_mult_less_cancel1"; |
14 val real_mult_less_cancel1 = thm"real_mult_less_cancel1"; |
31 val real_mult_le_cancel1 = thm"real_mult_le_cancel1"; |
15 val real_mult_le_cancel1 = thm"real_mult_le_cancel1"; |
32 val real_mult_eq_cancel1 = thm"real_mult_eq_cancel1"; |
16 val real_mult_eq_cancel1 = thm"real_mult_eq_cancel1"; |