diff options
Diffstat (limited to 'theories/Reals/ArithProp.v')
| -rw-r--r-- | theories/Reals/ArithProp.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index eab47da8e0..a5c5ddaf82 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -75,7 +75,7 @@ Proof. apply H3; assumption. right. apply H4; assumption. - unfold double in |- *; ring. + unfold double in |- *;ring. Qed. (* 2m <= 2n => m<=n *) |