proposition: Theorem ClosestOpp : forall (p : float) (r : R), Closest b radix r p -> Closest b radix (- r) (Fopp p).
proof: Proof. intros p r H'; split. apply oppBounded; auto. case H'; auto. intros f H'0. rewrite Fopp_correct. replace (- FtoR radix p - - r)%R with (- (FtoR radix p - r))%R; [ idtac | ring ]. replace (FtoR radix f - - r)%R with (- (- FtoR radix f - r))%R; [ idtac | ring ]. rewrite <- Fopp_correct. repeat rewrite Rabs_Ropp. apply H', oppBounded; easy. Qed.
imports: Reals ZArith List PeanoNat Psatz