proposition: Lemma is_limit_phi0 (alpha : Ord) : zero < alpha -> is_limit (phi0 alpha).
proof: Proof. intros H; split. - intro H0; case (@lt_irrefl zero). apply lt_le_trans with alpha;auto. rewrite <- H0; pattern phi0; apply phi0_elim. intros f H1; eapply ordering_le; [ eauto |]. split. - intro H0; destruct H0 as [x H0]. generalize (@AP_phi0 alpha). intro H1; destruct H1 as [H1 H2]; rewrite H0 in H2. assert (H3 : x < succ x) by auto with schutte. generalize (H2 _ H3); intros H4; assert (H5 :zero < x). { tricho zero x H8. - auto. - subst x; replace (succ zero) with (F 1) in H0. + rewrite <- phi0_zero in H0. case (@lt_irrefl (phi0 zero)). pattern (phi0 zero) at 2; rewrite <- H0. apply phi0_mono;auto. + simpl;auto. - case (@not_lt_zero x); auto. } assert (H6 : x < x + x). { pattern x at 1;rewrite <- alpha_plus_zero. apply plus_mono_r;auto. } generalize (succ_mono H6); rewrite <- H4. intros H7; apply lt_irrefl with (succ (x+x)); auto. now rewrite plus_of_succ in H7. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)