proposition: Theorem MinExList : forall (r : R) (L : list float), (forall f : float, In f L -> (r < f)%R) \/ (exists min : float, In min L /\ (min <= r)%R /\ (forall f : float, In f L -> (f <= r)%R -> (f <= min)%R)).
proof: Proof. intros r L; elim L; simpl in |- *; auto. left; intros f H'; elim H'. intros a l H'. elim H'; [ intros H'0; clear H' | intros H'0; elim H'0; intros min E; elim E; intros H'1 H'2; elim H'2; intros H'3 H'4; try exact H'4; clear H'2 E H'0 H' ]. case (Rle_or_lt a r); intros H'1. right; exists a; repeat split; auto. intros f H'; elim H'; [ intros H'2; rewrite <- H'2; clear H' | intros H'2; clear H' ]; auto with real. intros H'; contradict H'; auto with real. apply Rlt_not_le; auto with real. left; intros f H'; elim H'; [ intros H'2; rewrite <- H'2; clear H' | intros H'2; clear H' ]; auto. case (Rle_or_lt a min); intros H'5. right; exists min; repeat split; auto. intros f H'; elim H'; [ intros H'0; rewrite <- H'0; clear H' | intros H'0; clear H' ]; auto. case (Rle_or_lt a r); intros H'6. right; exists a; repeat split; auto. intros f H'; elim H'; [ intros H'0; rewrite <- H'0; clear H' | intros H'0; clear H' ]; auto with real. intros H'; apply Rle_trans with (FtoRradix min); auto with real. right; exists min; split; auto; split; auto. intros f H'; elim H'; [ intros H'0; elim H'0; clear H' | intros H'0; clear H' ]; auto. intros H'; contradict H'6; auto with real. apply Rle_not_lt; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz