Commit 35f2b3f4 authored by Heiko Becker's avatar Heiko Becker

Minor simplification of Errorbound

parent 3c8163c2
......@@ -17,8 +17,7 @@ Proof.
rewrite delta_0_deterministic; auto.
inversion eval_float; subst.
unfold perturb; simpl.
rewrite Rabs_err_simpl.
rewrite Rabs_mult.
rewrite Rabs_err_simpl, Rabs_mult.
apply Rmult_le_compat_l; [apply Rabs_pos | auto].
Qed.
......
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