remove lemmas nat_add_min_{left,right} in favor of generic lemmas min_add_distrib_{left,right}

--- a/src/HOL/Groups.thy	Thu Sep 08 18:13:48 2011 -0700
+++ b/src/HOL/Groups.thy	Thu Sep 08 18:47:23 2011 -0700
@@ -596,6 +596,14 @@
   "min x y + z = min (x + z) (y + z)"
   unfolding min_def by auto
 
+lemma max_add_distrib_right:
+  "x + max y z = max (x + y) (x + z)"
+  unfolding max_def by auto
+
+lemma min_add_distrib_right:
+  "x + min y z = min (x + y) (x + z)"
+  unfolding min_def by auto
+
 end
 
 subsection {* Support for reasoning about signs *}

--- a/src/HOL/Library/Saturated.thy	Thu Sep 08 18:13:48 2011 -0700
+++ b/src/HOL/Library/Saturated.thy	Thu Sep 08 18:47:23 2011 -0700
@@ -131,7 +131,7 @@
     case True thus ?thesis by (simp add: sat_eq_iff)
   next
     case False thus ?thesis
-      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib nat_add_min_left nat_add_min_right min_max.inf_assoc min_max.inf_absorb2)
+      by (simp add: sat_eq_iff nat_mult_min_left add_mult_distrib min_add_distrib_left min_add_distrib_right min_max.inf_assoc min_max.inf_absorb2)
   qed
 qed (simp_all add: sat_eq_iff mult.commute)
 

--- a/src/HOL/Nat.thy	Thu Sep 08 18:13:48 2011 -0700
+++ b/src/HOL/Nat.thy	Thu Sep 08 18:47:23 2011 -0700
@@ -753,16 +753,6 @@
    "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
 by (simp split: nat.split)
 
-lemma nat_add_min_left:
-  fixes m n q :: nat
-  shows "min m n + q = min (m + q) (n + q)"
-  by (simp add: min_def)
-
-lemma nat_add_min_right:
-  fixes m n q :: nat
-  shows "m + min n q = min (m + n) (m + q)"
-  by (simp add: min_def)
-
 lemma nat_mult_min_left:
   fixes m n q :: nat
   shows "min m n * q = min (m * q) (n * q)"