diff options
| author | Cyril Cohen | 2018-07-19 17:11:59 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2018-07-19 17:11:59 +0200 |
| commit | 47831fdfcc1aa313b722232cebde2d3607f2e9b2 (patch) | |
| tree | ec61d532976dcc89694239904ea79851fed178c9 /mathcomp | |
| parent | a4f169772ace822087c9ab6aaac3f81982560b97 (diff) | |
last_eq for exhaustivity
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 4bc704a..8938ac5 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -992,6 +992,9 @@ Proof. by move=> s0x; rewrite -(cat_take_drop n0 s) mem_cat /= s0x. Qed. Lemma mem_drop s x : x \in drop n0 s -> x \in s. Proof. by move=> s0'x; rewrite -(cat_take_drop n0 s) mem_cat /= s0'x orbT. Qed. +Lemma last_eq s z x y : x != y -> z != y -> (last x s == y) = (last z s == y). +Proof. by move=> /negPf xz /negPf yz; case: s => [|t s]//; rewrite xz yz. Qed. + Section Filters. Variable a : pred T. |