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/path.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/path.v')
| -rw-r--r-- | mathcomp/ssreflect/path.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v index d9ab11c..2790aa8 100644 --- a/mathcomp/ssreflect/path.v +++ b/mathcomp/ssreflect/path.v @@ -368,7 +368,7 @@ Proof. elim: s => [| h s]; first by case: ifP. rewrite mem2_cons => ->. do 2 rewrite inE (fun_if subseq) !if_arg !sub1seq /=. -by case: eqVneq => [->|]; case: eqVneq. +by have [->|] := eqVneq; case: eqVneq. Qed. Variant split2r x y : seq T -> Type := @@ -916,7 +916,7 @@ Let le_lex_transitive x sT : transitive (le_lex x sT). Proof. move=> ? ? ? /andP [xy /implyP xy'] /andP [yz /implyP yz']. rewrite /= (leT_tr xy yz) /=; apply/implyP => zx. -by apply/ltn_trans: (xy' (leT_tr yz zx)) (yz' (leT_tr zx xy)). +exact: ltn_trans (xy' (leT_tr yz zx)) (yz' (leT_tr zx xy)). Qed. Lemma filter_sort p s : filter p (sort leT s) = sort leT (filter p s). |