proposition: Lemma succ_monoR (alpha beta : Ord) : succ alpha < succ beta -> alpha < beta.
proof: Proof. intro H; tricho alpha beta t; auto with schutte. - subst beta; case (@lt_irrefl (succ alpha)); eauto with schutte. - case (@lt_irrefl (succ alpha)); eapply lt_trans;eauto. apply succ_mono;auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)