proposition: Lemma zero_le (alpha : Ord) : zero <= alpha.
proof: Proof. unfold zero, the_least, the; apply iota_ind. - apply the_least_unicity, Inh_ord. - destruct 1 as [[_ H1] _]; apply H1; split. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)