proposition: Lemma finite_plus_infinite (n : nat) (alpha : Ord) : omega <= alpha -> n + alpha = alpha.
proof: Proof. induction n. - simpl; intros;rewrite zero_plus_alpha;trivial. - intros; simpl; replace (succ (F n)) with (F 1 + F n). + rewrite <- plus_assoc. rewrite IHn. * apply one_plus_infinite; assumption. * assumption. + now rewrite <- plus_FF. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)