From bf18afeefa06e972c6cb98fa8a81ec7172fdde7f Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 20 May 2014 19:56:29 +0200 Subject: Moving (e)transitivity out of the AST. --- theories/Numbers/NatInt/NZSqrt.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'theories/Numbers') 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). -- cgit v1.2.3