proposition: Lemma one_plus_omega : 1 + omega = omega.
proof: Proof. rewrite plus_limit; auto with schutte. - apply le_antisym; auto with schutte. + unfold omega_limit; apply sup_mono;auto with schutte. * apply Ordering_Functions.R1 with ordinal (ge (F 1)). apply plus_ordering. apply countable_members;auto with schutte. red; split. * intros x [a [H1 H2]]. red in H1; case (@lt_omega_finite _ H1). intros n e; exists (F (S n)). subst x; split;auto with schutte. exists (S n); trivial. subst a. split;auto. subst a. left; now rewrite <- plus_FF . + unfold omega_limit; apply sup_mono. * apply seq_range_countable; auto with schutte. * simpl; auto with schutte. apply Ordering_Functions.R1 with ordinal (ge (succ zero)). apply plus_ordering; auto with schutte. apply countable_members; auto with schutte. red; split. * intros x [x0 [_ Hx]]; subst x. exists (F (S x0));split;auto with schutte. exists (F x0);split;auto with schutte. red; red; apply finite_lt_omega. rewrite <- plus_FF; trivial. - apply is_limit_omega. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles) ZornsLemma(CountableTypes)