proposition: Lemma AP_plus_AP (alpha beta gamma : Ord) : zero < beta -> phi0 alpha + beta = phi0 gamma -> alpha < gamma /\ beta = phi0 gamma.
proof: Proof. intros H H0; tricho alpha gamma H3. - split;auto. tricho beta (phi0 gamma) H4. + case (@lt_irrefl (phi0 gamma)). pattern (phi0 gamma) at 1; rewrite <- H0. * apply AP_plus_closed; auto. apply AP_phi0; eauto with schutte. apply phi0_mono;auto. + auto. + rewrite <- H0 in H4; case (@lt_irrefl beta). eapply le_lt_trans;eauto. apply le_plus_r. - subst gamma; case (@lt_irrefl (phi0 alpha)). pattern (phi0 alpha) at 2; rewrite <- H0. pattern (phi0 alpha) at 1; rewrite <- alpha_plus_zero. apply plus_mono_r;auto. - assert(H1 : phi0 alpha <= phi0 gamma). { rewrite <- H0; apply le_plus_l. } case (le_not_gt H1); apply phi0_mono;auto. Qed.
imports: Coq(Arith Logic.Epsilon Ensembles Lia) ZornsLemma(CountableTypes)