diff options
| author | Cyril Cohen | 2020-09-02 23:26:39 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-09-03 19:59:28 +0200 |
| commit | 667dd52bd039a96f896b81533b0aaafe98b9f8de (patch) | |
| tree | 413e131d444270f9d993437f13122e4aa5bc4277 | |
| parent | fbeec199e65fe7e9fd96ddd74e31aa0461c22927 (diff) | |
compat Coq < 8.10
| -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. |