src/HOL/Groups.thy

--- 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 *}