proposition: Lemma zero_le (alpha : Ord) : zero <= alpha.
proof: Proof. generalize (iota_spec inh_Ord _ R). destruct 1 as [_ H]; apply H; split. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)