proposition: Lemma the_least_ok : forall X : Ensemble Ord, Inhabited X -> forall a, In X a -> the_least X <= a.
proof: Proof. intros X H a H0; pattern X, (the_least X). unfold the_least, the;apply iota_ind. - apply the_least_unicity. now exists a. - intros a0 H2; destruct H2; now apply H1. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)