proposition: Lemma one_plus_infinite (alpha : Ord) : omega <= alpha -> 1 + alpha = alpha.
proof: Proof. intros H. generalize (minus_exists H); intros [gamma e]; subst alpha . rewrite plus_assoc. now rewrite one_plus_omega. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)