proposition: Theorem t_exact: (FtoRradix t=p-q)%R.
proof: Proof. unfold FtoRradix; rewrite <- Fminus_correct; auto with zarith. apply sym_eq; apply RoundedModeProjectorIdemEq with (b:=bo) (P:=(EvenClosest bo radix precision)) (precision:=precision); auto. apply EvenClosestRoundedModeP; auto. 2: rewrite Fminus_correct; auto with zarith. apply Sterbenz; auto. fold FtoRradix; apply Rmult_le_reg_l with 2%R; auto with real. apply Rle_trans with (FtoRradix q);[simpl; right; field; auto with real|idtac]. apply Q_le_two_P. fold FtoRradix; simpl; apply P_le_two_Q. Qed.
imports: Reals ZArith List PeanoNat Psatz