src/HOL/Nat.thy
changeset 36977 71c8973a604b
parent 36176 3fe7e97ccca8
child 37387 3581483cca6c
     1.1 --- a/src/HOL/Nat.thy	Mon May 17 18:51:25 2010 -0700
     1.2 +++ b/src/HOL/Nat.thy	Mon May 17 18:59:59 2010 -0700
     1.3 @@ -1294,15 +1294,11 @@
     1.4  begin
     1.5  
     1.6  lemma zero_le_imp_of_nat: "0 \<le> of_nat m"
     1.7 -  apply (induct m, simp_all)
     1.8 -  apply (erule order_trans)
     1.9 -  apply (rule ord_le_eq_trans [OF _ add_commute])
    1.10 -  apply (rule less_add_one [THEN less_imp_le])
    1.11 -  done
    1.12 +  by (induct m) simp_all
    1.13  
    1.14  lemma less_imp_of_nat_less: "m < n \<Longrightarrow> of_nat m < of_nat n"
    1.15    apply (induct m n rule: diff_induct, simp_all)
    1.16 -  apply (insert add_less_le_mono [OF zero_less_one zero_le_imp_of_nat], force)
    1.17 +  apply (rule add_pos_nonneg [OF zero_less_one zero_le_imp_of_nat])
    1.18    done
    1.19  
    1.20  lemma of_nat_less_imp_less: "of_nat m < of_nat n \<Longrightarrow> m < n"