proposition: Remark alpha_lt_beta : alpha < beta.
proof: Proof. Proof with auto with schutte. apply lt_trans with (seq 0). - simpl ... - unfold beta; apply lt_omega_limit ... Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)