Commit 3a861f71 authored by Guillaume Melquiond's avatar Guillaume Melquiond
Browse files

Simplified proofs.

parent bde8c0b0
......@@ -134,7 +134,7 @@ replace (bpow (Fexp fr)) with (ulp beta (FLX_exp prec) (F2R fr)).
rewrite <- Hr1.
apply ulp_error_f.
now apply FLX_exp_correct.
clear; unfold monotone_exp_prop; intros; unfold FLX_exp; omega.
apply FLX_exp_monotone.
exact Hr.
unfold ulp; apply f_equal.
now rewrite Hr2, <- Hr1.
......@@ -248,7 +248,7 @@ apply Rle_trans with (/2*ulp beta (FLX_exp prec) (F2R fr))%R.
rewrite <- Hr1.
apply ulp_half_error_f; trivial.
now apply FLX_exp_correct.
clear; unfold monotone_exp_prop; intros; unfold FLX_exp; omega.
apply FLX_exp_monotone.
right; unfold ulp; apply f_equal.
rewrite Hr2, <- Hr1; trivial.
rewrite Rmult_assoc, Rmult_comm.
......
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