diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-20 19:56:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-20 20:03:00 +0200 |
| commit | bf18afeefa06e972c6cb98fa8a81ec7172fdde7f (patch) | |
| tree | 78b737079c541e425c160506d9b80577f389f091 /theories/Numbers | |
| parent | b6fea49600a5b6089eeeea877f06f0e197a0eafb (diff) | |
Moving (e)transitivity out of the AST.
Diffstat (limited to 'theories/Numbers')
| -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). |