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