# HG changeset patch
# User paulson
# Date 929003695 -7200
# Node ID 52b13dfbe9548b584a687675b13e18d409100873
# Parent  66dc8e62a987f29b7c06d4305b8237c1cfb8c402
new lemma less_Suc_eq_0_disj

diff -r 66dc8e62a987 -r 52b13dfbe954 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Thu Jun 10 10:24:32 1999 +0200
+++ b/src/HOL/Nat.ML	Thu Jun 10 10:34:55 1999 +0200
@@ -54,6 +54,12 @@
 qed "not_gr0";
 AddIffs [not_gr0];
 
+(*Useful in certain inductive arguments*)
+Goal "(m < Suc n) = (m=0 | (EX j. m = Suc j & j < n))";
+by (exhaust_tac "m" 1);
+by Auto_tac;
+qed "less_Suc_eq_0_disj";
+
 qed_goalw "Least_Suc" thy [Least_nat_def]
  "!!P. [| ? n. P(Suc n); ~ P 0 |] ==> (LEAST n. P n) = Suc (LEAST m. P(Suc m))"
  (fn _ => [