proposition: Lemma maxlist_less : forall x l, 0 < length l -> (forall y, member y l -> y [<] x) -> maxlist l [<] x.
proof: Proof. simple induction l. simpl in |- *; intros; exfalso; inversion H. clear l. do 2 intro. intro H. clear H; induction l as [| a0 l Hrecl]. simpl in |- *; intros H H0. apply H0; right; algebra. generalize l a0 Hrecl; clear Hrecl l a0. intros l b; intros. rename X into H0. eapply less_wdl. 2: apply maxlist_aux. astepl (Max b (maxlist (cons a l))). apply Max_less. apply H0; left; right; algebra. apply Hrecl. simpl in |- *; apply Nat.lt_0_succ. intros y H1. apply H0. inversion_clear H1. left; left; assumption. right; assumption. Qed.
imports: CoRN.reals.CReals1