proposition: Lemma lt_succ_lt (alpha beta : Ord) : is_limit beta -> alpha < beta -> succ alpha < beta.
proof: Proof. intros (Hbeta, Hbeta') H; case (lt_succ_le H); [|auto]. - intros H' ; subst ; case Hbeta'. exists alpha;split; eauto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)