proposition: Lemma le_disj : forall alpha beta, alpha <= beta -> alpha = beta \/ alpha < beta.
proof: Proof. intros alpha beta H; destruct H; tauto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)