1053 lemmas real_mult_inverse_left = left_inverse [of "x::real", standard] |
1053 lemmas real_mult_inverse_left = left_inverse [of "x::real", standard] |
1054 lemmas INVERSE_ZERO = inverse_zero [where 'a=real] |
1054 lemmas INVERSE_ZERO = inverse_zero [where 'a=real] |
1055 lemmas real_le_refl = order_refl [of "w::real", standard] |
1055 lemmas real_le_refl = order_refl [of "w::real", standard] |
1056 lemmas real_le_antisym = order_antisym [of "z::real" "w", standard] |
1056 lemmas real_le_antisym = order_antisym [of "z::real" "w", standard] |
1057 lemmas real_le_trans = order_trans [of "i::real" "j" "k", standard] |
1057 lemmas real_le_trans = order_trans [of "i::real" "j" "k", standard] |
|
1058 lemmas real_le_linear = linear [of "z::real" "w", standard] |
1058 lemmas real_le_eq_diff = le_iff_diff_le_0 [of "x::real" "y", standard] |
1059 lemmas real_le_eq_diff = le_iff_diff_le_0 [of "x::real" "y", standard] |
1059 lemmas real_add_left_mono = add_left_mono [of "x::real" "y" "z", standard] |
1060 lemmas real_add_left_mono = add_left_mono [of "x::real" "y" "z", standard] |
1060 lemmas real_mult_order = mult_pos_pos [of "x::real" "y", standard] |
1061 lemmas real_mult_order = mult_pos_pos [of "x::real" "y", standard] |
1061 lemmas real_mult_less_mono2 = |
1062 lemmas real_mult_less_mono2 = |
1062 mult_strict_left_mono [of "x::real" "y" "z", COMP swap_prems_rl, standard] |
1063 mult_strict_left_mono [of "x::real" "y" "z", COMP swap_prems_rl, standard] |