Commit 2ef9988e authored by Guillaume Melquiond's avatar Guillaume Melquiond

Homogenize theorem names from Ulp.

parent d8ce723c
......@@ -281,7 +281,7 @@ rewrite Rabs_left in Hh; try assumption.
assert (0 < pred_flt f).
apply Rlt_le_trans with (bpow emin).
apply bpow_gt_0.
apply le_pred_lt...
apply pred_ge_gt...
apply FLT_format_bpow...
omega.
apply Rlt_le_trans with (2:=H1).
......
This diff is collapsed.
......@@ -209,7 +209,7 @@ destruct (Req_dec x' 0) as [Zx'|Nzx'].
* rewrite <- (Rabs_right x) at 1; [|now apply Rle_ge; apply Rlt_le].
apply bpow_mag_gt.
- exact Vfexp1.
- exact Px'. }
- now apply Rlt_le. }
fold (cexp beta fexp2 x); fold (ulp beta fexp2 x).
assert (/ 2 * ulp beta fexp1 x <= ulp beta fexp1 x).
rewrite <- (Rmult_1_l (ulp _ _ _)) at 2.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment