src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Thu Dec 18 15:06:24 2003 +0100
+++ b/src/HOL/Nat.thy	Fri Dec 19 04:28:45 2003 +0100
@@ -268,6 +268,12 @@
   apply (blast intro: Suc_mono less_SucI elim: lessE)
   done
 
+text {* "Less than" is antisymmetric, sort of *}
+lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
+apply(simp only:less_Suc_eq)
+apply blast
+done
+
 lemma nat_neq_iff: "((m::nat) \<noteq> n) = (m < n | n < m)"
   using less_linear by blast