proposition: Theorem ClosestMin : forall (r : R) (min max : float), isMin b radix r min -> isMax b radix r max -> (2 * r <= min + max)%R -> Closest r min.
proof: Proof. intros r min max H' H'0 H'1; split. case H'; auto. intros f H'2. case (Rle_or_lt f r); intros H'3. repeat rewrite Rabs_left1. apply Ropp_le_contravar. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. case H'; auto. intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply isMin_inv1 with (1 := H'); auto. rewrite (Rabs_left1 (min - r)). rewrite (Rabs_right (f - r)). apply Rle_trans with (max - r)%R. cut (forall x y : R, (- y + x)%R = (- (y - x))%R); [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ]. cut (forall x y : R, (- (x - y))%R = (y - x)%R); [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; unfold Rminus in |- *; ring ]. apply Rplus_le_reg_l with (r := FtoR radix min). repeat rewrite Rplus_minus; auto. apply Rplus_le_reg_l with (r := r). replace (r + (FtoR radix min + (max - r)))%R with (min + max)%R. replace (r + r)%R with (2 * r)%R; auto. simpl in |- *; ring. simpl in |- *; fold FtoRradix; ring. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. case H'0; auto. intros H'4 H'5; elim H'5; intros H'6 H'7; apply H'7; clear H'5; auto. apply Rlt_le; auto. apply Rle_ge; apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rlt_le; auto. apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply isMin_inv1 with (1 := H'); auto. Qed.
imports: Reals ZArith List PeanoNat Psatz