proposition: Theorem ClosestMinEq : forall (r : R) (min max p : float), isMin b radix r min -> isMax b radix r max -> (2 * r < min + max)%R -> Closest r p -> p = min :>R.
proof: Proof. intros r min max p H' H'0 H'1 H'2. case (ClosestMinOrMax r p); auto; intros H'3. unfold FtoRradix in |- *; apply MinEq with (1 := H'3); auto. absurd (Rabs (max - r) <= Rabs (min - r))%R. apply Rgt_not_le. rewrite (Rabs_left1 (min - r)). rewrite Rabs_right. replace (- (min - r))%R with (r - min)%R; [ idtac | ring ]. red in |- *; apply Rplus_lt_reg_l with (r := FtoRradix min). repeat rewrite Rplus_minus; auto. apply Rplus_lt_reg_l with (r := r). replace (r + r)%R with (2 * r)%R; [ idtac | simpl in |- *; ring ]. replace (r + (min + (max - r)))%R with (min + max)%R; [ idtac | ring ]; auto. apply Rle_ge; apply Rplus_le_reg_l with (r := r). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply isMax_inv1 with (1 := H'0); 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. cut (Closest r max). intros H'4; case H'4. intros H'5 H'6; apply H'6; auto. case H'; auto. apply ClosestCompatible with (1 := H'2); auto. apply MaxEq with (1 := H'3); auto. case H'0; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz