--- a/src/HOL/Fields.thy Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Fields.thy Mon Apr 09 15:20:11 2018 +0100
@@ -46,6 +46,14 @@
lemmas [arith_split] = nat_diff_split split_min split_max
+context linordered_nonzero_semiring
+begin
+lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)"
+ by (auto simp: max_def)
+
+lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)"
+ by (auto simp: min_def)
+end
text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>