diff options
| author | Cyril Cohen | 2020-01-03 14:45:53 +0100 |
|---|---|---|
| committer | GitHub | 2020-01-03 14:45:53 +0100 |
| commit | c7fa2a1444d450bcebdeea47800fef1436690b6d (patch) | |
| tree | e0cf42c9b4b8ad39ddec274a368e1f6800b9cc49 /mathcomp/ssreflect/seq.v | |
| parent | a93a392121e8e02c6fdaa6c674dd90af8b12c28d (diff) | |
| parent | a06d61a8e226eeabc52f1a22e469dca1e6077065 (diff) | |
Merge pull request #443 from pi8027/eqVneq
Refactoring and linting proofs especially in polydiv.v
Diffstat (limited to 'mathcomp/ssreflect/seq.v')
| -rw-r--r-- | mathcomp/ssreflect/seq.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v index 0ddd382..5b9d047 100644 --- a/mathcomp/ssreflect/seq.v +++ b/mathcomp/ssreflect/seq.v @@ -429,7 +429,7 @@ Qed. Lemma set_set_nth s n1 y1 n2 y2 (s2 := set_nth s n2 y2) : set_nth (set_nth s n1 y1) n2 y2 = if n1 == n2 then s2 else set_nth s2 n1 y1. Proof. -have [-> | ne_n12] := altP eqP. +have [-> | ne_n12] := eqVneq. apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnA maxnn. by do 2!rewrite !nth_set_nth /=; case: eqP. apply: eq_from_nth => [|i _]; first by rewrite !size_set_nth maxnCA. @@ -2239,7 +2239,7 @@ Lemma nth_index_map s x0 x : {in s &, injective f} -> x \in s -> nth x0 s (index (f x) (map f s)) = x. Proof. elim: s => //= y s IHs inj_f s_x; rewrite (inj_in_eq inj_f) ?mem_head //. -move: s_x; rewrite inE; case: eqVneq => [-> | _] //=; apply: IHs. +move: s_x; rewrite inE; have [-> // | _] := eqVneq; apply: IHs. by apply: sub_in2 inj_f => z; apply: predU1r. Qed. |