proposition: Theorem ClosestMinOrMax : MinOrMaxP b radix Closest.
proof: Proof. red in |- *. intros r p H'. case (Rle_or_lt p r); intros H'1. left; split; auto. case H'; auto. split; auto. intros f H'0 H'2. apply Rplus_le_reg_l with (r := (- r)%R). cut (forall x y : R, (- y + x)%R = (- (y - x))%R); [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ]. apply Ropp_le_contravar. rewrite <- (Rabs_right (r - FtoR radix p)). rewrite <- (Rabs_right (r - FtoR radix f)). cut (forall x y : R, Rabs (x - y) = Rabs (y - x)); [ intros Eq0; repeat rewrite (Eq0 r); clear Eq0 | intros x y; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr ]; auto. elim H'; auto. apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix f). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rle_ge; apply Rplus_le_reg_l with (r := FtoR radix p). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. right; split; auto. case H'; auto. split; auto. apply Rlt_le; auto. intros f H'0 H'2. apply Rplus_le_reg_l with (r := (- r)%R). cut (forall x y : R, (- y + x)%R = (- (y - x))%R); [ intros Eq0; repeat rewrite Eq0; clear Eq0 | intros; ring ]. rewrite <- (Rabs_left1 (r - FtoR radix p)). rewrite <- (Rabs_left1 (r - FtoR radix f)). cut (forall x y : R, Rabs (x - y) = Rabs (y - x)); [ intros Eq0; repeat rewrite (Eq0 r); clear Eq0 | intros x y; rewrite <- (Rabs_Ropp (x - y)); rewrite Ropp_minus_distr ]; auto. elim H'; auto. apply Rplus_le_reg_l with (r := FtoR radix f). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rplus_le_reg_l with (r := FtoR radix p). repeat rewrite Rplus_minus; auto. rewrite Rplus_0_r; auto. apply Rlt_le; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz