proposition: Lemma lt_succ_le (alpha beta : Ord): alpha < beta -> succ alpha <= beta.
proof: Proof. Proof with eauto with schutte. intros H; pattern (succ alpha); apply the_least_ok ... exists (succ alpha); red;apply lt_succ ... Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)