diff options
Diffstat (limited to 'theories/Reals')
| -rw-r--r-- | theories/Reals/RIneq.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index dd2108159..8bebb5237 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -2017,7 +2017,7 @@ Proof. Qed. Lemma R_rm : ring_morph - R0 R1 Rplus Rmult Rminus Ropp eq + 0%R 1%R Rplus Rmult Rminus Ropp eq 0%Z 1%Z Zplus Zmult Zminus Zopp Zeq_bool IZR. Proof. constructor ; try easy. |