proposition: Theorem MinEx : forall r : R, exists min : float, isMin r min.
proof: Proof. intros r. case (MinExList r (mBFloat r)). intros H'0; absurd (Fopp (boundR r) <= r)%R; auto. apply Rlt_not_le. apply H'0. apply mBFadic_correct3; auto. apply Rlt_le. apply boundRCorrect2; auto. intros H'0; elim H'0; intros min E; elim E; intros H'1 H'2; elim H'2; intros H'3 H'4; clear H'2 E H'0. exists min; split; auto. apply mBPadic_Fbounded with (r := r); auto. split; auto. intros f H'0 H'2. case (Req_dec f 0); intros H'6. replace (FtoRradix f) with (FtoRradix (Float 0 (- dExp b))). apply H'4; auto. apply mBFadic_correct4; auto. replace (FtoRradix (Float 0 (- dExp b))) with (FtoRradix f); auto. rewrite H'6. unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real. rewrite H'6. unfold FtoRradix, FtoR in |- *; simpl in |- *; auto with real. case (Rle_or_lt f (Fopp (boundR r))); intros H'5. apply Rle_trans with (FtoRradix (Fopp (boundR r))); auto. apply H'4; auto. apply mBFadic_correct3; auto. apply Rlt_le. apply boundRCorrect2; auto. case (Rle_or_lt (boundR r) f); intros H'7. contradict H'2; apply Rlt_not_le. apply Rlt_le_trans with (FtoRradix (boundR r)); auto. apply boundRCorrect1; auto. apply H'4; auto. apply mBFadic_correct1; auto. contradict H'6; unfold FtoRradix in |- *; apply is_Fzero_rep1; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz