proposition: Lemma not_lt_zero : forall alpha, ~ alpha < zero.
proof: Proof. intros;apply le_not_gt; apply zero_le;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)