src/HOL/Nat.thy
changeset 51263 31e786e0e6a7
parent 51173 3cbb4e95a565
child 51329 4a3c453f99a1
     1.1 --- a/src/HOL/Nat.thy	Sun Feb 24 20:18:32 2013 +0100
     1.2 +++ b/src/HOL/Nat.thy	Sun Feb 24 20:29:13 2013 +0100
     1.3 @@ -1201,6 +1201,16 @@
     1.4      apply (auto)
     1.5    done
     1.6  
     1.7 +lemma mono_times_nat:
     1.8 +  fixes n :: nat
     1.9 +  assumes "n > 0"
    1.10 +  shows "mono (times n)"
    1.11 +proof
    1.12 +  fix m q :: nat
    1.13 +  assume "m \<le> q"
    1.14 +  with assms show "n * m \<le> n * q" by simp
    1.15 +qed
    1.16 +
    1.17  text {* the lattice order on @{typ nat} *}
    1.18  
    1.19  instantiation nat :: distrib_lattice