proposition: Lemma minlist_leEq_eps : forall l : list IR, {x : IR | member x l} -> forall e, [0] [<] e -> {x : IR | member x l | x [<=] minlist l[+]e}.
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 He. simpl in |- *; exists a. right; algebra. apply less_leEq; apply shift_less_plus'. astepl ZeroR; assumption. cut ({a0 [<=] Min a0 (minlist (cons a l)) [+]e [/]TwoNZ} + {minlist (cons a l) [<=] Min a0 (minlist (cons a l)) [+]e [/]TwoNZ}). 2: apply leEq_Min_plus_eps; apply pos_div_two; assumption. intro H1. elim H1; intro H2. exists a0. simpl in |- *; left; right; algebra. apply leEq_transitive with (Min a (minlist (cons a0 l)) [+]e [/]TwoNZ). apply shift_leEq_plus. astepr (minlist (cons a (cons a0 l))). eapply leEq_wdr. 2: apply minlist_aux. astepr (Min a0 (minlist (cons a l))). apply shift_minus_leEq; assumption. astepr (Min a (minlist (cons a0 l)) [+]e). apply plus_resp_leEq_lft. apply less_leEq; apply pos_div_two'; assumption. elim Hrecl with (e [/]TwoNZ). intros x p q. exists x. elim p; intro H3. left; left; assumption. right; assumption. apply shift_leEq_plus; eapply leEq_wdr. 2: apply minlist_aux. apply shift_minus_leEq. astepr (Min a0 (minlist (cons a l)) [+]e). rstepr (Min a0 (minlist (cons a l)) [+]e [/]TwoNZ[+]e [/]TwoNZ). apply leEq_transitive with (minlist (cons a l) [+]e [/]TwoNZ). assumption. apply plus_resp_leEq; assumption. exists a; right; algebra. apply pos_div_two; assumption. Qed.
imports: CoRN.reals.CReals1