proposition: Lemma maxlist_leEq : forall y l, 0 < length l -> (forall x, member x l -> x [<=] y) -> maxlist l [<=] y.
proof: Proof. simple induction l. simpl in |- *; intros; exfalso; inversion H. clear l. do 3 intro. clear H; induction l as [| a0 l Hrecl]. simpl in |- *; intros. apply H0; right; algebra. generalize l a0 Hrecl; clear Hrecl l a0. intros l b; intros. eapply leEq_wdl. 2: apply maxlist_aux. astepl (Max b (maxlist (cons a l))). apply Max_leEq. apply H0; left; right; algebra. apply Hrecl. simpl in |- *; auto with arith. intros x H1. apply H0. inversion_clear H1. left; left; assumption. right; assumption. Qed.
imports: CoRN.reals.CReals1