634 lemma le_diff_eq[algebra_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c" |
634 lemma le_diff_eq[algebra_simps]: "a \<le> c - b \<longleftrightarrow> a + b \<le> c" |
635 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel) |
635 by (auto simp add: le_less less_diff_eq diff_add_cancel add_diff_cancel) |
636 |
636 |
637 lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0" |
637 lemma le_iff_diff_le_0: "a \<le> b \<longleftrightarrow> a - b \<le> 0" |
638 by (simp add: algebra_simps) |
638 by (simp add: algebra_simps) |
639 |
|
640 lemma sum_nonneg_eq_zero_iff: |
|
641 assumes x: "0 \<le> x" and y: "0 \<le> y" |
|
642 shows "(x + y = 0) = (x = 0 \<and> y = 0)" |
|
643 proof - |
|
644 have "x + y = 0 \<Longrightarrow> x = 0" |
|
645 proof - |
|
646 from y have "x + 0 \<le> x + y" by (rule add_left_mono) |
|
647 also assume "x + y = 0" |
|
648 finally have "x \<le> 0" by simp |
|
649 then show "x = 0" using x by (rule antisym) |
|
650 qed |
|
651 moreover have "x + y = 0 \<Longrightarrow> y = 0" |
|
652 proof - |
|
653 from x have "0 + y \<le> x + y" by (rule add_right_mono) |
|
654 also assume "x + y = 0" |
|
655 finally have "y \<le> 0" by simp |
|
656 then show "y = 0" using y by (rule antisym) |
|
657 qed |
|
658 ultimately show ?thesis by auto |
|
659 qed |
|
660 |
639 |
661 text{*Legacy - use @{text algebra_simps} *} |
640 text{*Legacy - use @{text algebra_simps} *} |
662 lemmas group_simps[noatp] = algebra_simps |
641 lemmas group_simps[noatp] = algebra_simps |
663 |
642 |
664 end |
643 end |