proposition: Lemma zero_or_greater : forall alpha : Ord, alpha = zero \/ exists beta, beta < alpha.
proof: Proof. intros a; tricho zero a t;auto with schutte. - right;exists zero;auto with schutte. - case (not_lt_zero t). Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)