proposition: Lemma lt_succ_le_2 (alpha beta : Ord): alpha < succ beta -> alpha <= beta.
proof: Proof. intro H; tricho alpha beta t;eauto with schutte. case (@lt_irrefl alpha); apply lt_le_trans with (succ beta). - assumption. - apply lt_succ_le;eauto with schutte. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)