proposition: Lemma nf_bounded beta l alpha : alpha <= phi0 beta -> is_cnf_of alpha l -> exponents_le beta l.
proof: Proof. revert alpha; elim l. - constructor. - intros a l0 H alpha H0 H1; right. + case H1;intros H3; simpl in H3. intro ; subst alpha; apply phi0_mono_R_weak. apply le_trans with (phi0 a + eval l0);auto. apply le_plus_l. + apply H with (eval l0). * case H1; intros H2 H3; simpl in H3. apply le_trans with alpha. -- subst alpha; apply le_plus_r. -- auto with schutte. * split; [ | trivial]. case H1; inversion 1; auto with schutte. Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)