proposition: Lemma phi0_mono_weak (alpha beta : Ord) : alpha <= beta -> phi0 alpha <= phi0 beta.
proof: Proof. destruct 1. - subst beta; auto with schutte. - right;apply phi0_mono;auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)