diff options
| author | Kazuhiko Sakaguchi | 2020-05-13 13:11:14 +0900 |
|---|---|---|
| committer | Kazuhiko Sakaguchi | 2020-05-13 14:09:09 +0900 |
| commit | 35bd8708dacfb508f896d957d7b1189ca7decb3e (patch) | |
| tree | 32cfd78b33e69dca564f42df40bfa5a3ec93b4e5 /mathcomp/ssreflect/tuple.v | |
| parent | 3515b33b1245ea169fbaf61405dc60954509fee2 (diff) | |
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`.
Diffstat (limited to 'mathcomp/ssreflect/tuple.v')
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |