diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-03-10 16:39:53 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2014-03-10 16:39:53 +0100 |
| commit | 6a59faaddbefc0326a3071d81942ae4cc0dd0300 (patch) | |
| tree | d39f7fab19d64cc81e3d835c7bf21e6c1cdc031b /theories/Reals | |
| parent | 643e624909ecec7ba43326ff962b13c184991125 (diff) | |
Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.
Diffstat (limited to 'theories/Reals')
| -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 2472f4c3c..b444d443d 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. |