proposition: Lemma cnf_lt_epsilon0 : forall l alpha, is_cnf_of alpha l -> alpha < epsilon0 -> Forall (fun beta => beta < alpha) l.
proof: Proof. induction l. - constructor. - unfold is_cnf_of. destruct 1 as [H e]. intro H0; simpl. assert (Hlt : a < phi0 a). { apply lt_phi0; simpl in e; subst alpha; apply le_lt_trans with (phi0 a); auto with schutte. - apply le_phi0. - apply le_lt_trans with (2 := H0); apply le_plus_l. } simpl in e; constructor. subst alpha; apply lt_le_trans with (1 := Hlt). + apply le_plus_l. + specialize (IHl (eval l)); unfold is_cnf_of in IHl. apply Forall_impl with (fun o => o < eval l). * intros a0 H1; apply lt_le_trans with (1 := H1). subst alpha; apply le_plus_r. * apply IHl . { split; auto ; eapply sorted_tail; eauto. } apply le_lt_trans with (2 := H0). subst alpha; apply (le_plus_r). Qed.
imports: Coq(Arith List Sorting.Sorted Logic.Epsilon Ensembles)