proposition: Lemma exponents_lt_eval alpha l: exponents_lt alpha l -> eval l < phi0 alpha.
proof: Proof. induction 1; cbn. - apply phi0_positive. - apply AP_plus_closed; trivial. + apply AP_phi0; auto. + apply phi0_mono;auto. Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)