From 35bd8708dacfb508f896d957d7b1189ca7decb3e Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Wed, 13 May 2020 13:11:14 +0900
Subject: Revise proofs in ssreflect/*.v

This change reduces
- use of numerical occurrence selectors (#436) and
- use of non ssreflect tactics such as `auto`,
and improves use of comparison predicates such as `posnP`, `leqP`, `ltnP`,
`ltngtP`, and `eqVneq`.
---
 mathcomp/ssreflect/tuple.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp/ssreflect/tuple.v')

diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 551dc77..db53235 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -351,8 +351,8 @@ rewrite count_filter -(@eq_count _ (pred1 t)) => [|s /=]; last first.
   by rewrite isSome_insub; case: eqP=> // ->.
 elim: n t t_n => [|m IHm] [|x t] //= {IHm}/IHm; move: (iter m _ _) => em IHm.
 transitivity (x \in T : nat); rewrite // -mem_enum codomE.
-elim: (fintype.enum T)  (enum_uniq T) => //= y e IHe /andP[/negPf ney].
-rewrite count_cat count_map inE /preim /= {1}/eq_op /= eq_sym => /IHe->.
+elim: (fintype.enum T) (enum_uniq T) => //= y e IHe /andP[/negPf ney].
+rewrite count_cat count_map inE /preim /= [in LHS]/eq_op /= eq_sym => /IHe->.
 by case: eqP => [->|_]; rewrite ?(ney, count_pred0, IHm).
 Qed.
 
-- 
cgit v1.2.3