Commit a473371d authored by Heiko Becker's avatar Heiko Becker

Temp fix for 8.7.2 compat

parent e7cc1ef7
......@@ -86,13 +86,13 @@ Proof.
apply Rabs_triang; apply Rplus_le_compat; try auto.
rewrite Rplus_0_r.
apply Rplus_le_compat; try auto. }
4: {
eapply Rle_trans.
apply Rabs_triang. setoid_rewrite Rplus_assoc at 2.
apply Rplus_le_compat; try auto.
eapply Rle_trans.
apply Rabs_triang.
rewrite Rabs_Ropp. apply Rplus_le_compat; auto. }
Focus 4.
eapply Rle_trans; [ apply Rabs_triang | rewrite (Rplus_assoc (Q2R err1)) ].
apply Rplus_le_compat; try auto.
eapply Rle_trans; [ apply Rabs_triang |].
apply Rplus_le_compat; try auto.
rewrite Rabs_Ropp; simpl. auto.
all: eapply Rle_trans; try eapply H.
all: setoid_rewrite Rplus_assoc at 2.
all: eapply Rplus_le_compat; try auto.
......@@ -165,7 +165,7 @@ Proof.
apply Rplus_le_compat; try auto.
rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym.
auto. }
4: {
Focus 4.
eapply Rle_trans.
apply Rabs_triang. setoid_rewrite Rplus_assoc at 2.
apply Rplus_le_compat; try auto.
......@@ -173,7 +173,8 @@ Proof.
apply Rabs_triang.
rewrite Rabs_Ropp. apply Rplus_le_compat; try auto.
rewrite Rplus_comm, <- Rsub_eq_Ropp_Rplus, Rabs_minus_sym.
auto. }
auto.
all: eapply Rle_trans; try eapply Rabs_triang.
all: setoid_rewrite Rplus_assoc at 2.
all: eapply Rplus_le_compat; try auto.
......@@ -340,13 +341,14 @@ Proof.
unfold computeErrorR.
destruct m; rewrite Ropp_plus_distr.
{ rewrite Rplus_0_r; hnf; right; f_equal; lra. }
4: {
rewrite <- Rplus_assoc.
eapply Rle_trans.
eapply Rabs_triang.
rewrite Rabs_Ropp.
eapply Rplus_le_compat; try auto.
hnf; right; f_equal; lra. }
Focus 4.
rewrite <- Rplus_assoc.
eapply Rle_trans.
eapply Rabs_triang.
rewrite Rabs_Ropp.
eapply Rplus_le_compat; try auto.
hnf; right; f_equal; lra.
all: repeat rewrite <- Rplus_assoc.
all: setoid_rewrite <- Rsub_eq_Ropp_Rplus at 2.
all: repeat rewrite Rsub_eq_Ropp_Rplus.
......
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