proposition: Theorem ClosestIdem : forall p q : float, Fbounded b p -> Closest b radix p q -> p = q :>R.
proof: Proof. intros p q H' H'0. case (Rabs_pos (q - p)); intros H1. contradict H1; apply Rle_not_lt. replace 0%R with (Rabs (p - p)); [ case H'0; auto | idtac ]. replace (p - p)%R with 0%R; [ apply Rabs_R0; auto | ring ]. apply Rplus_eq_reg_l with (r := (- p)%R). apply trans_eq with 0%R; [ ring | idtac ]. apply trans_eq with (q - p)%R; [ idtac | ring ]. generalize H1; unfold Rabs in |- *; case (Rcase_abs (q - p)); auto. intros r H0; replace 0%R with (-0)%R; [ rewrite H0 | idtac ]; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz