proposition: Theorem IneqEq: (FtoRradix v=u)%R.
proof: Proof. assert (u <= v)%R; auto with real. generalize (EvenClosestMonotone bo radix precision); unfold MonotoneP. intros L; apply L with (3 * Rabs (p - q))%R (p+q)%R; auto; clear L. generalize (EvenClosestCompatible bo radix precision); unfold CompatibleP. intros L. apply L with (3*Rabs t)%R u; auto. replace (FtoRradix t) with (p-q)%R; auto with real. apply sym_eq; unfold FtoRradix, radix; apply t_exact with bo precision b b'; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz