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/fingroup | |
| 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/fingroup')
| -rw-r--r-- | mathcomp/fingroup/perm.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v index b35ab1d..34f230e 100644 --- a/mathcomp/fingroup/perm.v +++ b/mathcomp/fingroup/perm.v @@ -475,7 +475,7 @@ have [|ts def_s ne_ts] := IHn (tperm x (s^-1 x) * s); last first. rewrite (cardD1 x) !inE s_x in le_s_n; apply: leq_ltn_trans le_s_n. apply: subset_leq_card; apply/subsetP=> y. rewrite !inE permM permE /= -(canF_eq (permK _)). -have [-> | ne_yx] := altP (y =P x); first by rewrite permKV eqxx. +have [-> | ne_yx] := eqVneq y x; first by rewrite permKV eqxx. by case: (s y =P x) => // -> _; rewrite eq_sym. Qed. |