proposition: Lemma phi0_alpha_phi0_beta (alpha beta: Ord) : alpha < beta -> phi0 alpha + phi0 beta = phi0 beta.
proof: Proof. intros. apply plus_lt_phi0; eauto with schutte. apply phi0_mono. auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)