# HG changeset patch
# User paulson
# Date 968233657 -7200
# Node ID c7049cb55a119e279b4d6ab6245f802685f7817a
# Parent  53e2a8bce258e927152159cfe8a9299fff7ceda0
new Iff theorem zero_le_succ_iff

diff -r 53e2a8bce258 -r c7049cb55a11 src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Wed Sep 06 08:39:31 2000 +0200
+++ b/src/ZF/Ordinal.ML	Wed Sep 06 11:47:37 2000 +0200
@@ -475,10 +475,16 @@
 by (blast_tac (claset() addIs [Ord_0_lt]) 1);
 qed "Ord_0_lt_iff";
 
+
 (*** Results about less-than or equals ***)
 
 (** For ordinals, j<=i (subset) implies j le i (less-than or equals) **)
 
+Goal "0 le succ(x) <-> Ord(x)";
+by (blast_tac (claset() addIs [Ord_0_le] addEs [ltE]) 1); 
+qed "zero_le_succ_iff";
+AddIffs [zero_le_succ_iff];
+
 Goal "[| j<=i;  Ord(i);  Ord(j) |] ==> j le i";
 by (rtac (not_lt_iff_le RS iffD1) 1);
 by (assume_tac 1);