src/HOL/Nat.thy
changeset 27679 6392b92c3536
parent 27627 93016de79b02
child 27789 1bf827e3258d
     1.1 --- a/src/HOL/Nat.thy	Fri Jul 25 07:35:53 2008 +0200
     1.2 +++ b/src/HOL/Nat.thy	Fri Jul 25 12:03:28 2008 +0200
     1.3 @@ -391,19 +391,12 @@
     1.4  instance
     1.5  proof
     1.6    fix n m :: nat
     1.7 -  have less_imp_le: "n < m \<Longrightarrow> n \<le> m"
     1.8 -    unfolding less_eq_Suc_le by (erule Suc_leD)
     1.9 -  have irrefl: "\<not> m < m" by (induct m) auto
    1.10 -  have strict: "n \<le> m \<Longrightarrow> n \<noteq> m \<Longrightarrow> n < m"
    1.11 +  show "n < m \<longleftrightarrow> n \<le> m \<and> \<not> m \<le> n" 
    1.12    proof (induct n arbitrary: m)
    1.13 -    case 0 then show ?case
    1.14 -      by (cases m) (simp_all add: less_eq_Suc_le)
    1.15 +    case 0 then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
    1.16    next
    1.17 -    case (Suc n) then show ?case
    1.18 -      by (cases m) (simp_all add: less_eq_Suc_le)
    1.19 +    case (Suc n) then show ?case by (cases m) (simp_all add: less_eq_Suc_le)
    1.20    qed
    1.21 -  show "n < m \<longleftrightarrow> n \<le> m \<and> n \<noteq> m"
    1.22 -    by (auto simp add: irrefl intro: less_imp_le strict)
    1.23  next
    1.24    fix n :: nat show "n \<le> n" by (induct n) simp_all
    1.25  next