equal
deleted
inserted
replaced
523 apply (blast intro: elim: order_less_asym) |
523 apply (blast intro: elim: order_less_asym) |
524 done |
524 done |
525 |
525 |
526 lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)" |
526 lemma real_mult_le_cancel_iff2 [simp]: "(0::real) < z ==> (z*x \<le> z*y) = (x\<le>y)" |
527 by(simp add:mult_commute) |
527 by(simp add:mult_commute) |
528 |
|
529 (* FIXME: redundant, but used by Integration/Integral.thy in AFP *) |
|
530 lemma real_le_add_order: "[| 0 \<le> x; 0 \<le> y |] ==> (0::real) \<le> x + y" |
|
531 by (rule add_nonneg_nonneg) |
|
532 |
528 |
533 lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x" |
529 lemma real_inverse_gt_one: "[| (0::real) < x; x < 1 |] ==> 1 < inverse x" |
534 by (simp add: one_less_inverse_iff) (* TODO: generalize/move *) |
530 by (simp add: one_less_inverse_iff) (* TODO: generalize/move *) |
535 |
531 |
536 |
532 |