proposition: Lemma le_alpha_zero (alpha : Ord) : alpha <= zero -> alpha = zero.
proof: Proof. intros H; apply le_antisym;auto. apply zero_le. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)