equal
deleted
inserted
replaced
314 |
314 |
315 lemma real_le_add_right_cancel: "!!(A::real). A + C \<le> B + C ==> A \<le> B" |
315 lemma real_le_add_right_cancel: "!!(A::real). A + C \<le> B + C ==> A \<le> B" |
316 by (rule Ring_and_Field.add_le_imp_le_right) |
316 by (rule Ring_and_Field.add_le_imp_le_right) |
317 |
317 |
318 lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B" |
318 lemma real_le_add_left_cancel: "!!(A::real). C + A \<le> C + B ==> A \<le> B" |
319 by (rule (*Ring_and_Field.*)add_le_imp_le_left) |
319 by (rule Ring_and_Field.add_le_imp_le_left) |
320 |
320 |
321 lemma real_add_right_cancel_less: "(v+z < w+z) = (v < (w::real))" |
321 lemma real_add_right_cancel_less: "(v+z < w+z) = (v < (w::real))" |
322 by (rule Ring_and_Field.add_less_cancel_right) |
322 by (rule Ring_and_Field.add_less_cancel_right) |
323 |
323 |
324 lemma real_add_left_cancel_less: "(z+v < z+w) = (v < (w::real))" |
324 lemma real_add_left_cancel_less: "(z+v < z+w) = (v < (w::real))" |