--- a/Quot/Examples/LarryInt.thy	Mon Feb 15 16:50:11 2010 +0100
+++ b/Quot/Examples/LarryInt.thy	Mon Feb 15 16:52:32 2010 +0100
@@ -1,7 +1,7 @@
 
 header{*The Integers as Equivalence Classes over Pairs of Natural Numbers*}
 
-theory LarryInt 
+theory LarryInt
 imports Nat "../Quotient" "../Quotient_Product"
 begin
 
@@ -373,12 +373,14 @@
   "nat_raw"
 
 abbreviation
-  "less_raw x y \<equiv> (le_raw x y \<and> \<not>(x = y))"
+  "less_raw x y \<equiv> (le_raw x y \<and> \<not>(intrel x y))"
 
 lemma nat_le_eq_zle_raw:
   shows "less_raw (0, 0) w \<or> le_raw (0, 0) z \<Longrightarrow> (nat_raw w \<le> nat_raw z) = (le_raw w z)"
-apply(auto)
-sorry
+  apply (cases w)
+  apply (cases z)
+  apply (simp add: nat_raw_def le_raw_def)
+  by auto
 
 lemma [quot_respect]:
   shows "(intrel ===> op =) nat_raw nat_raw"