src/HOL/Orderings.thy

     and "\<And>y. P y \<Longrightarrow> x \<le> y"
     and "\<And>x. P x \<Longrightarrow> \<forall>y. P y \<longrightarrow> x \<le> y \<Longrightarrow> Q x"
   shows "Q (Least P)"
 unfolding Least_def by (rule theI2)
   (blast intro: assms antisym)+
-
 
 text \<open>Dual order\<close>
 
 lemma dual_order:
   "class.order (op \<ge>) (op >)"

   by (simp add:min_def)
 
 lemma max_absorb1: "(y::'a::order) \<le> x \<Longrightarrow> max x y = x"
   by (simp add: max_def)
 
+lemma max_min_same [simp]:
+  fixes x y :: "'a :: linorder"
+  shows "max x (min x y) = x" "max (min x y) x = x" "max (min x y) y = y" "max y (min x y) = y"
+by(auto simp add: max_def min_def)
 
 subsection \<open>(Unique) top and bottom elements\<close>
 
 class bot =
   fixes bot :: 'a ("\<bottom>")