proposition: Lemma seq_mono_intro (s: nat -> Ord) : (forall i, s i < s (S i)) -> seq_mono s.
proof: Proof. intros H; unfold seq_mono; induction 1; auto. apply (@Lt_trans Ord lt AX1) with (s m);auto. Qed.
imports: Coq(Relations Classical Classical_sets) ZornsLemma(CountableTypes) hydras(Well_Orders Lub Countable)