proposition: Theorem ImplyClosestStrict2: (Rabs(z-f) < (powerRZ radix e)/2)%R -> (Closest b radix z f) /\ (forall g: float, Closest b radix z g -> (FtoRradix f=g)%R ).
proof: Proof. intros; split. apply ImplyClosest; auto with real. apply ImplyClosestStrict; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz