From e2fb620d4a2bb6da26d344b69f22befdde09b1d0 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt
Date: Wed, 16 Sep 2020 01:33:27 +0900
Subject: comparable_big lemma in order.v

---
 mathcomp/algebra/ssrnum.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/algebra')

diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index c28aec2..36498b3 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1786,8 +1786,8 @@ Lemma min_real : {in real &, forall x y, min x y \is real}.
 Proof. by move=> x y ? ?; case: real_leP. Qed.
 
 Lemma bigmax_real I x0 (r : seq I) (P : pred I) (f : I -> R):
-  x0 \is real -> {in P, forall t : I, f t \is real} ->
-  \big[max/x0]_(t <- r | P t) f t \is real.
+  x0 \is real -> {in P, forall i : I, f i \is real} ->
+  \big[max/x0]_(i <- r | P i) f i \is real.
 Proof.
 by move=> x0r Pr; elim/big_rec : _ => // i x Pi xr; rewrite max_real ?Pr.
 Qed.
-- 
cgit v1.2.3