proposition: Remark lt_beta_exists : exists n, ksi < seq n.
proof: Proof. case (@lt_omega_limit_lt_exists_lt ksi seq mono_seq); auto. intros;exists x;auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)