diff options
| author | Cyril Cohen | 2020-11-26 10:39:02 +0100 |
|---|---|---|
| committer | GitHub | 2020-11-26 10:39:02 +0100 |
| commit | 3af5647929406b754ea44aaac34678abc646451d (patch) | |
| tree | 48cf82ccbe66fa77ad975608fc1c85f4384312c9 | |
| parent | be8fee1c8c9ca7eff75475d51506f9631b7499f4 (diff) | |
| parent | f2f5b83e8e6a6157cd980017cd4248a4f945ab95 (diff) | |
Merge pull request #678 from CohenCyril/under_fix
Using under and removing comment
| -rw-r--r-- | mathcomp/ssreflect/bigop.v | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v index 50f05d2..c1f420f 100644 --- a/mathcomp/ssreflect/bigop.v +++ b/mathcomp/ssreflect/bigop.v @@ -1536,11 +1536,7 @@ 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))/=. - (** 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 under eq_bigl do rewrite liftK eq_sym eqxx neq_lift ?andbT. by move=> i; case: unliftP => [k ->|->]; rewrite ?eqxx ?andbF. Qed. |