diff options
| author | Cyril Cohen | 2018-12-13 15:05:06 +0100 |
|---|---|---|
| committer | GitHub | 2018-12-13 15:05:06 +0100 |
| commit | f962d2a88254a99bffbc7d0a40949872a80f4669 (patch) | |
| tree | 60a84ff296299226d530dd0b495be24fd7675748 /mathcomp/ssreflect/tuple.v | |
| parent | fa9b7b19fc0409f3fdfa680e08f40a84594e8307 (diff) | |
| parent | 0b1ea03dafcf36880657ba910eec28ab78ccd018 (diff) | |
Merge pull request #262 from math-comp/cancel-lemmas-implicit
Cancel lemmas implicit
Diffstat (limited to 'mathcomp/ssreflect/tuple.v')
| -rw-r--r-- | mathcomp/ssreflect/tuple.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v index 9154eb5..8f81155 100644 --- a/mathcomp/ssreflect/tuple.v +++ b/mathcomp/ssreflect/tuple.v @@ -336,7 +336,7 @@ Definition enum : seq (n.-tuple T) := Lemma enumP : Finite.axiom enum. Proof. -case=> /= t t_n; rewrite -(count_map _ (pred1 t)) (pmap_filter (@insubK _ _ _)). +case=> /= t t_n; rewrite -(count_map _ (pred1 t)) (pmap_filter (insubK _)). 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. |