proposition: Lemma not_AP_inv_0 : forall alpha, zero < alpha -> ~ (AP alpha) -> exists beta,zero < beta /\ beta < alpha /\ alpha < beta + alpha .
proof: Proof. Proof with eauto with schutte. intros alpha H H0; apply Classical_Prop.NNPP. intro H1;apply H0; split ... intros beta H2; tricho (beta+alpha) alpha H3 ... - case (@lt_irrefl alpha). apply le_lt_trans with (beta+alpha) ... apply le_plus_r ... - case H1; exists beta; split ; auto. tricho zero beta H4; auto with schutte. + subst beta; rewrite zero_plus_alpha in H3; case (@lt_irrefl alpha);auto. + now case (@not_lt_zero beta). Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)