proposition: Lemma omega_tower_mono (i : nat) : omega_tower i < omega_tower (S i).
proof: Proof. induction i; simpl. - rewrite succ_is_plus_1, zero_plus_alpha; rewrite <- omega_eqn; apply finite_lt_omega. - simpl in IHi; now apply phi0_mono. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)