proposition: Lemma epsilon0_fxp : phi0 epsilon0 = epsilon0.
proof: Proof. unfold epsilon0, omega_limit; rewrite phi0_sup. assert (D1: Countable (image (seq_range omega_tower) phi0)). { apply countable_image. apply seq_range_countable. } assert (D2: Countable (seq_range omega_tower)). { apply Countable.seq_range_countable. } - apply le_antisym. + apply sup_mono; trivial. * destruct 1 as [x0 [[i [_ H]] H0]]. exists (phi0 x0); split. { exists (S i); split; auto; simpl; auto ; now f_equal. } left; auto. + apply sup_mono; trivial. intros alpha [i H]; exists (phi0 alpha); split; auto. exists alpha; split; auto. * exists i; auto. * apply le_phi0. - exists (phi0 zero), 0; simpl; rewrite phi0_zero; split; auto. - apply Countable.seq_range_countable. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)