proposition: Lemma not_AP_inv2 : forall alpha, zero < alpha -> ~AP alpha -> exists beta, exists gamma, zero < beta /\ zero < gamma /\ beta < alpha /\ gamma < alpha /\ alpha = beta + gamma.
proof: Proof. Proof with eauto with schutte. intros alpha H H0; case (not_AP_inv_0 H H0). intros khi [Hkhi H'khi]; exists khi. case (minus_exists (alpha:=khi) (beta:= alpha)) ... - destruct H'khi. right;auto. - intros eta H2; exists eta; split ; auto. split;auto. + tricho zero eta H3; trivial. * subst eta; rewrite alpha_plus_zero in H2; trivial. decompose [and] H'khi; subst alpha; case (@lt_irrefl khi);auto. * case (@not_lt_zero eta) ... + decompose [and] H'khi; split;auto. split;auto. tricho zero khi H5 ... tricho eta alpha H6 ... subst eta; case (@lt_irrefl (khi+alpha)) ... case (@lt_irrefl (khi + eta)) ... apply lt_trans with (khi+alpha) ... apply plus_mono_r ... subst khi; case (@lt_irrefl zero);auto. case (@not_lt_zero khi) ... Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)