proposition: Lemma sorted_lt l alpha: sorted (alpha::l) -> eval l < phi0 alpha + eval l.
proof: Proof. revert alpha; induction l. - inversion 1; simpl; rewrite alpha_plus_zero; apply phi0_positive;auto. - inversion 1; simpl; rewrite plus_assoc. generalize (IHl _ H2); intro H5. apply le_lt_trans with (phi0 alpha + eval l). + apply plus_mono_weak_l. now apply phi0_mono_weak. + rewrite <- plus_assoc; now apply plus_mono_r. Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)