proposition: Lemma zero_lt_succ : forall alpha, zero < succ alpha.
proof: Proof. intros a; apply le_lt_trans with a;eauto with schutte; apply zero_le;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)