From a06d61a8e226eeabc52f1a22e469dca1e6077065 Mon Sep 17 00:00:00 2001
From: Kazuhiko Sakaguchi
Date: Fri, 29 Nov 2019 01:19:33 +0900
Subject: Refactoring and linting especially polydiv

- Replace `altP eqP` and `altP (_ =P _)` with `eqVneq`:
  The improved `eqVneq` lemma (#351) is redesigned as a comparison predicate and
  introduces a hypothesis in the form of `x != y` in the second case. Thus,
  `case: (altP eqP)`, `case: (altP (x =P _))` and `case: (altP (x =P y))` idioms
  can be replaced with `case: eqVneq`, `case: (eqVneq x)` and
  `case: (eqVneq x y)` respectively. This replacement slightly simplifies and
  reduces proof scripts.
- use `have [] :=` rather than `case` if it is better.
- `by apply:` -> `exact:`.
- `apply/lem1; apply/lem2` or `apply: lem1; apply: lem2` -> `apply/lem1/lem2`.
- `move/lem1; move/lem2` -> `move/lem1/lem2`.
- Remove `GRing.` prefix if applicable.
- `negbTE` -> `negPf`, `eq_refl` -> `eqxx` and `sym_equal` -> `esym`.
---
 mathcomp/field/algC.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'mathcomp/field/algC.v')

diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index 0e3005d..4932148 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -166,7 +166,7 @@ have normD x y : le (norm (x + y)) (norm x + norm y).
     have [-> | nz_u u_ge0 v_ge0] := eqVneq u 0; first by rewrite add0r.
     by have /andP[]: lt 0 (u + v) by rewrite sposDl // /lt nz_u.
   have le_sqr u v: conj u = u -> le 0 v -> le (u ^+ 2) (v ^+ 2) -> le u v.
-    move=> Ru v_ge0; have [-> // | nz_u] := eqVneq u 0.
+    case: (eqVneq u 0) => [-> //|nz_u Ru v_ge0].
     have [u_gt0 | u_le0 _] := boolP (lt 0 u).
       by rewrite leB (leB u) subr_sqr mulrC addrC; apply: sposM; apply: sposDl.
     rewrite leB posD // posE normN -addr_eq0; apply/eqP.
@@ -931,7 +931,7 @@ Qed.
 
 Lemma dvdCP x y : reflect (exists2 z, z \in Cint & y = z * x) (x %| y)%C.
 Proof.
-rewrite unfold_in; have [-> | nz_x] := altP eqP.
+rewrite unfold_in; have [-> | nz_x] := eqVneq.
   by apply: (iffP eqP) => [-> | [z _ ->]]; first exists 0; rewrite ?mulr0.
 apply: (iffP idP) => [Zyx | [z Zz ->]]; last by rewrite mulfK.
 by exists (y / x); rewrite ?divfK.
@@ -990,7 +990,7 @@ Canonical dvdC_zmodPred x := ZmodPred (dvdC_zmod x).
 Lemma dvdC_nat (p n : nat) : (p %| n)%C = (p %| n)%N.
 Proof.
 rewrite unfold_in CintEge0 ?divr_ge0 ?invr_ge0 ?ler0n // !pnatr_eq0.
-have [-> | nz_p] := altP eqP; first by rewrite dvd0n.
+have [-> | nz_p] := eqVneq; first by rewrite dvd0n.
 apply/CnatP/dvdnP=> [[q def_q] | [q ->]]; exists q.
   by apply/eqP; rewrite -eqC_nat natrM -def_q divfK ?pnatr_eq0.
 by rewrite [num in num / _]natrM mulfK ?pnatr_eq0.
-- 
cgit v1.2.3