# HG changeset patch
# User lcp
# Date 797765457 -7200
# Node ID a53cbb4b06c555bb5f7f1b1c0ea8c2f4c5cb07b1
# Parent  1d8fa2fc4b9ca5fa0b8cee60847d722e62cccd21
Proved lesspoll_succ_iff.

diff -r 1d8fa2fc4b9c -r a53cbb4b06c5 src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Thu Apr 13 10:20:55 1995 +0200
+++ b/src/ZF/Cardinal.ML	Thu Apr 13 11:30:57 1995 +0200
@@ -188,7 +188,7 @@
 by (REPEAT (eresolve_tac [asm_rl, ltE] 1));
 qed "less_LeastE";
 
-(*Easier to apply than LeastI2: conclusion has only one occurrence of P*)
+(*Easier to apply than LeastI: conclusion has only one occurrence of P*)
 qed_goal "LeastI2" Cardinal.thy
     "[| P(i);  Ord(i);  !!j. P(j) ==> Q(j) |] ==> Q(LEAST j. P(j))"
  (fn prems => [ resolve_tac prems 1, 
@@ -440,6 +440,11 @@
 by (fast_tac (ZF_cs addSIs [inj_not_surj_succ]) 1);
 qed "lesspoll_succ_imp_lepoll";
 
+goal Cardinal.thy "!!m. m:nat ==> A lesspoll succ(m) <-> A lepoll m";
+by (fast_tac (ZF_cs addSIs [lepoll_imp_lesspoll_succ, 
+			    lesspoll_succ_imp_lepoll]) 1);
+qed "lesspoll_succ_iff";
+
 goal Cardinal.thy "!!A m. [| A lepoll succ(m);  m:nat |] ==>  \
 \                         A lepoll m | A eqpoll succ(m)";
 by (rtac disjCI 1);