src/HOL/Nat.thy
changeset 44848 f4d0b060c7ca
parent 44817 b63e445c8f6d
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Nat.thy	Thu Sep 08 18:13:48 2011 -0700
     1.2 +++ b/src/HOL/Nat.thy	Thu Sep 08 18:47:23 2011 -0700
     1.3 @@ -753,16 +753,6 @@
     1.4     "max m (Suc n) = (case m of 0 => Suc n | Suc m' => Suc(max m' n))"
     1.5  by (simp split: nat.split)
     1.6  
     1.7 -lemma nat_add_min_left:
     1.8 -  fixes m n q :: nat
     1.9 -  shows "min m n + q = min (m + q) (n + q)"
    1.10 -  by (simp add: min_def)
    1.11 -
    1.12 -lemma nat_add_min_right:
    1.13 -  fixes m n q :: nat
    1.14 -  shows "m + min n q = min (m + n) (m + q)"
    1.15 -  by (simp add: min_def)
    1.16 -
    1.17  lemma nat_mult_min_left:
    1.18    fixes m n q :: nat
    1.19    shows "min m n * q = min (m * q) (n * q)"