diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZSqrt.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZSqrt.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v index 8146fd014..6b6c85310 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -438,7 +438,7 @@ Instance sqrt_up_wd : Proper (eq==>eq) sqrt_up. Proof. assert (Proper (eq==>eq==>Logic.eq) compare). intros x x' Hx y y' Hy. do 2 case compare_spec; trivial; order. - intros x x' Hx. unfold sqrt_up. rewrite Hx. case compare; now rewrite ?Hx. + intros x x' Hx; unfold sqrt_up; rewrite Hx; case compare; now rewrite ?Hx. Qed. (** The spec of [sqrt_up] indeed determines it *) |