Commit 6bc1a0dd authored by Heiko Becker's avatar Heiko Becker

Fix theorem placement, broken by refactoring

parent 9894803f
......@@ -113,18 +113,6 @@ Proof.
all: rewrite Rabs_eq_Qabs; auto.
Qed.
Lemma computeErrorR_up (v a b:R) m:
(Rabs v <= RmaxAbsFun (a,b))%R ->
(computeErrorR v m <= computeErrorR (RmaxAbsFun (a,b)) m)%R.
Proof.
intros.
unfold computeErrorR; destruct m; try lra.
all:apply Rmult_le_compat_r; try auto using mTypeToR_pos_R.
all:unfold RmaxAbsFun in *.
all:setoid_rewrite Rabs_right at 2; try auto.
all:apply Rle_ge; rewrite Rmax_Rle; auto using Rabs_pos.
Qed.
Open Scope R_scope.
Lemma mTypeToR_pos_R m:
......@@ -137,6 +125,18 @@ Proof.
apply pow_lt; lra.
Qed.
Lemma computeErrorR_up (v a b:R) m:
Rabs v <= RmaxAbsFun (a,b) ->
computeErrorR v m <= computeErrorR (RmaxAbsFun (a,b)) m.
Proof.
intros.
unfold computeErrorR; destruct m; try lra.
all:apply Rmult_le_compat_r; try auto using mTypeToR_pos_R.
all:unfold RmaxAbsFun in *.
all:setoid_rewrite Rabs_right at 2; try auto.
all:apply Rle_ge; rewrite Rmax_Rle; auto using Rabs_pos.
Qed.
Close Scope R_scope.
Lemma mTypeToQ_pos_Q m:
......
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