src/ZF/Nat.ML
changeset 484 70b789956bd3
parent 435 ca5356bd315a
child 760 f0200e91b272
--- a/src/ZF/Nat.ML	Thu Jul 21 16:51:26 1994 +0200
+++ b/src/ZF/Nat.ML	Tue Jul 26 13:21:20 1994 +0200
@@ -95,6 +95,15 @@
 by (etac ltD 1);
 val Limit_nat = result();
 
+goal Nat.thy "!!i. Limit(i) ==> nat le i";
+by (resolve_tac [subset_imp_le] 1);
+by (rtac subsetI 1);
+by (eresolve_tac [nat_induct] 1);
+by (fast_tac (ZF_cs addIs [Limit_has_succ RS ltD, ltI, Limit_is_Ord]) 2);
+by (REPEAT (ares_tac [Limit_has_0 RS ltD,
+		      Ord_nat, Limit_is_Ord] 1));
+val nat_le_Limit = result();
+
 (* succ(i): nat ==> i: nat *)
 val succ_natD = [succI1, asm_rl, Ord_nat] MRS Ord_trans;