proposition: Lemma not_is_succ_limit (alpha : Ord) : is_limit alpha -> ~ is_succ alpha.
proof: Proof. unfold is_limit;tauto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)