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