diff options
| -rw-r--r-- | theories/Reals/RIneq.v | 16 |
1 files changed, 15 insertions, 1 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 2472f4c3c7..b444d443d0 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -415,7 +415,14 @@ Hint Resolve f_equal_R : real. Lemma Rplus_eq_compat_l : forall r r1 r2, r1 = r2 -> r + r1 = r + r2. Proof. - auto with real. + intros r r1 r2. + apply f_equal. +Qed. + +Lemma Rplus_eq_compat_r : forall r r1 r2, r1 = r2 -> r1 + r = r2 + r. +Proof. + intros r r1 r2. + apply (f_equal (fun v => v + r)). Qed. (*i Old i*)Hint Resolve Rplus_eq_compat_l: v62. @@ -431,6 +438,13 @@ Proof. Qed. Hint Resolve Rplus_eq_reg_l: real. +Lemma Rplus_eq_reg_r : forall r r1 r2, r1 + r = r2 + r -> r1 = r2. +Proof. + intros r r1 r2 H. + apply Rplus_eq_reg_l with r. + now rewrite 2!(Rplus_comm r). +Qed. + (**********) Lemma Rplus_0_r_uniq : forall r r1, r + r1 = r -> r1 = 0. Proof. |