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 6b6c85310..f49c51e1e 100644 --- a/theories/Numbers/NatInt/NZSqrt.v +++ b/theories/Numbers/NatInt/NZSqrt.v @@ -66,7 +66,7 @@ Qed. Lemma sqrt_unique : forall a b, b² <= a < (S b)² -> √a == b. Proof. intros a b (LEb,LTb). - assert (Ha : 0<=a) by (transitivity b²; trivial using square_nonneg). + assert (Ha : 0<=a) by (transitivity (b²); trivial using square_nonneg). assert (Hb : 0<=b) by (apply sqrt_spec_nonneg; order). assert (Ha': 0<=√a) by now apply sqrt_nonneg. destruct (sqrt_spec a Ha) as (LEa,LTa). |