proposition: Lemma maxlist_leEq_eps : forall l : list IR, {x : IR | member x l} -> forall e, [0] [<] e -> {x : IR | member x l | maxlist l[-]e [<=] x}.
proof: Proof. intro l; induction l as [| a l Hrecl]. intro H; simpl in H; inversion H as [x H0]; inversion H0. clear Hrecl. intro H; induction l as [| a0 l Hrecl]; intros e H0. simpl in |- *; exists a. right; algebra. apply less_leEq; apply shift_minus_less; apply shift_less_plus'. astepl ZeroR; assumption. cut ({Max a0 (maxlist (cons a l)) [-]e [/]TwoNZ [<=] a0} + {Max a0 (maxlist (cons a l)) [-]e [/]TwoNZ [<=] maxlist (cons a l)}). 2: apply Max_minus_eps_leEq; apply pos_div_two; assumption. intro H1. elim H1; intro H2. exists a0. simpl in |- *; left; right; algebra. apply leEq_transitive with (Max a (maxlist (cons a0 l)) [-]e [/]TwoNZ). astepl (Max a (maxlist (cons a0 l)) [-]e). apply shift_leEq_minus; apply shift_plus_leEq'. rstepr e. apply less_leEq; apply pos_div_two'; assumption. apply shift_minus_leEq. astepl (maxlist (cons a (cons a0 l))). eapply leEq_wdl. 2: apply maxlist_aux. astepl (Max a0 (maxlist (cons a l))). apply shift_leEq_plus; assumption. elim Hrecl with (e [/]TwoNZ). intros x p q. exists x. elim p; intro H3. left; left; assumption. right; assumption. apply shift_minus_leEq; eapply leEq_wdl. 2: apply maxlist_aux. apply shift_leEq_plus. astepl (Max a0 (maxlist (cons a l)) [-]e). rstepl (Max a0 (maxlist (cons a l)) [-]e [/]TwoNZ[-]e [/]TwoNZ). apply leEq_transitive with (maxlist (cons a l) [-]e [/]TwoNZ). apply minus_resp_leEq; assumption. assumption. exists a; right; algebra. apply pos_div_two; assumption. Qed.
imports: CoRN.reals.CReals1