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`.

1 files changed, 1 insertions, 1 deletions

diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 8bdbe60..53a933a 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -1480,7 +1480,7 @@ Proof.
 move=> h'K; have [n lePn] := ubnP #|P|; elim: n => // n IHn in P h'K lePn *.
 case: (pickP P) => [i Pi | P0]; last first.
   by rewrite !big_pred0 // => j; rewrite P0.
-rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eq_refl //=; congr (_ * _).
+rewrite (bigD1 i Pi) (bigD1 (h' i)) h'K ?Pi ?eqxx //=; congr (_ * _).
 rewrite {}IHn => [|j /andP[]|]; [|by auto | by rewrite (cardD1x i) in lePn]. 
 apply: eq_bigl => j; rewrite andbC -andbA (andbCA (P _)); case: eqP => //= hK.
 by congr (_ && ~~ _); apply/eqP/eqP=> [<-|->] //; rewrite h'K.