src/HOL/Fields.thy
changeset 67969 83c8cafdebe8
parent 67091 1393c2340eec
child 68527 2f4e2aab190a
child 68536 e14848001c4c
     1.1 --- a/src/HOL/Fields.thy	Sun Apr 08 12:31:08 2018 +0200
     1.2 +++ b/src/HOL/Fields.thy	Mon Apr 09 15:20:11 2018 +0100
     1.3 @@ -46,6 +46,14 @@
     1.4  
     1.5  lemmas [arith_split] = nat_diff_split split_min split_max
     1.6  
     1.7 +context linordered_nonzero_semiring
     1.8 +begin
     1.9 +lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)"
    1.10 +  by (auto simp: max_def)
    1.11 +
    1.12 +lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)"
    1.13 +  by (auto simp: min_def)
    1.14 +end
    1.15  
    1.16  text\<open>Lemmas \<open>divide_simps\<close> move division to the outside and eliminates them on (in)equalities.\<close>
    1.17