diff options
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index ee3aedb..405ee08 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1509,7 +1509,11 @@ Lemma bigD1_ord n j (P : pred 'I_n) F : = F j * \big[*%M/1]_(i < n.-1 | P (lift j i)) F (lift j i). Proof. move=> Pj; rewrite (bigD1 j Pj) (reindex_omap (lift j) (unlift j))/=. - by under eq_bigl do rewrite liftK eq_sym eqxx neq_lift ?andbT. + (** Coq >= 8.10 *) + (* by under eq_bigl do rewrite liftK eq_sym eqxx neq_lift ?andbT. *) + (** Coq >= 8.7 *) + congr (_ * _); apply: eq_bigl => i. + by rewrite liftK eq_sym eqxx neq_lift ?andbT. by move=> i; case: unliftP => [k ->|->]; rewrite ?eqxx ?andbF. Qed. |