proposition: Lemma sorted_lt_lt (beta: Ord) : forall l alpha, sorted (cons alpha l) -> alpha < beta -> eval (cons alpha l) < phi0 beta.
proof: Proof. induction l. - simpl; inversion_clear 1. intro H;apply AP_plus_closed. + apply AP_phi0;eauto with schutte. + apply phi0_mono;eauto with schutte. + apply phi0_positive. - inversion 1; simpl; simpl in IHl. intro; apply AP_plus_closed. + apply AP_phi0;eauto with schutte. + apply phi0_mono;eauto with schutte. + apply IHl. * inversion H; auto. * eauto with schutte. Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)