diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 601dfb3b9d..e35d2c81ec 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -854,7 +854,7 @@ Proof. by rewrite unlock; elim: r => //= j r ->. Qed.
 Lemma big_nth x0 r (P : pred I) F :
   \big[op/idx]_(i <- r | P i) F i
      = \big[op/idx]_(0 <= i < size r | P (nth x0 r i)) (F (nth x0 r i)).
-Proof. by rewrite -{1}(mkseq_nth x0 r) big_map /index_iota subn0. Qed.
+Proof. by rewrite -[r in LHS](mkseq_nth x0) big_map /index_iota subn0. Qed.
 
 Lemma big_hasC r (P : pred I) F :
   ~~ has P r -> \big[op/idx]_(i <- r | P i) F i = idx.
@@ -949,9 +949,7 @@ Proof. by move=> ge_m_n; rewrite /index_iota (eqnP ge_m_n) big_nil. Qed.
 Lemma big_ltn_cond m n (P : pred nat) F :
     m < n -> let x := \big[op/idx]_(m.+1 <= i < n | P i) F i in
   \big[op/idx]_(m <= i < n | P i) F i = if P m then op (F m) x else x.
-Proof.
-by case: n => [//|n] le_m_n; rewrite /index_iota subSn // big_cons.
-Qed.
+Proof. by case: n => [//|n] le_m_n; rewrite /index_iota subSn // big_cons. Qed.
 
 Lemma big_ltn m n F :
      m < n ->
@@ -1329,7 +1327,7 @@ Lemma perm_big (I : eqType) r1 r2 (P : pred I) F :
 Proof.
 move/permP; rewrite !(big_mkcond _ _ P).
 elim: r1 r2 => [|i r1 IHr1] r2 eq_r12.
-  by case: r2 eq_r12 => // i r2; move/(_ (pred1 i)); rewrite /= eqxx.
+  by case: r2 eq_r12 => // i r2 /(_ (pred1 i)); rewrite /= eqxx.
 have r2i: i \in r2 by rewrite -has_pred1 has_count -eq_r12 /= eqxx.
 case/splitPr: r2 / r2i => [r3 r4] in eq_r12 *; rewrite big_cat /= !big_cons.
 rewrite mulmCA; congr (_ * _); rewrite -big_cat; apply: IHr1 => a.
@@ -1548,10 +1546,10 @@ Lemma pair_big_dep (I J : finType) (P : pred I) (Q : I -> pred J) F :
   \big[*%M/1]_(i | P i) \big[*%M/1]_(j | Q i j) F i j =
     \big[*%M/1]_(p | P p.1 && Q p.1 p.2) F p.1 p.2.
 Proof.
-rewrite (partition_big (fun p => p.1) P) => [|j]; last by case/andP.
-apply: eq_bigr => i /= Pi; rewrite (reindex_onto (pair i) (fun p => p.2)).
+rewrite (partition_big fst P) => [|j]; last by case/andP.
+apply: eq_bigr => i /= Pi; rewrite (reindex_onto (pair i) snd).
    by apply: eq_bigl => j; rewrite !eqxx [P i]Pi !andbT.
-by case=> i' j /=; case/andP=> _ /=; move/eqP->.
+by case=> i' j /= /andP [_] /eqP ->.
 Qed.
 
 Lemma pair_big (I J : finType) (P : pred I) (Q : pred J) F :
diff --git a/mathcomp/ssreflect/binomial.v b/mathcomp/ssreflect/binomial.v
index aef8e27859..d419745fb5 100644
--- a/mathcomp/ssreflect/binomial.v
+++ b/mathcomp/ssreflect/binomial.v
@@ -80,8 +80,7 @@ have vFpV i: i != Fp0 -> mFp (vFp i) i = Fp1.
   rewrite coprime_sym prime_coprime //; apply/negP=> /(dvdn_leq i_gt0).
   by rewrite leqNgt ltn_ord.
 have vFp0 i: i != Fp0 -> vFp i != Fp0.
-  move/vFpV=> inv_i; apply/eqP=> vFp0.
-  by have:= congr1 val inv_i; rewrite vFp0 /= mod0n.
+  by move/vFpV; apply/contra_eq_neq => ->; rewrite -val_eqE /= mul0n mod0n.
 have vFpK: {in predC1 Fp0, involutive vFp}.
   move=> i n0i; rewrite /= -[vFp _]mFp1r -(vFpV _ n0i) mFpA.
   by rewrite vFpV (vFp0, mFp1).
@@ -90,16 +89,16 @@ have le_pmFp (i : 'I_p) m: i <= p + m.
 have eqFp (i j : 'I_p): (i == j) = (p %| p + i - j).
   by rewrite -eqn_mod_dvd ?(modnDl, Fp_mod).
 have vFpId i: (vFp i == i :> nat) = xpred2 Fp1 Fpn1 i.
-  symmetry; have [->{i} | /eqP ni0] := i =P Fp0.
-    by rewrite /= -!val_eqE /= -{2}[p]prednK //= modn_small //= -(subnKC lt1p).
-  rewrite 2!eqFp -Euclid_dvdM //= -[_ - p.-1]subSS prednK //.
+  have [->{i} | ni0] := eqVneq i Fp0.
+    by rewrite -!val_eqE /= egcd0n modn_small //= -(subnKC lt1p).
+  rewrite 2!eqFp -Euclid_dvdM // -[_ - p.-1]subSS prednK //.
   have lt0i: 0 < i by rewrite lt0n.
   rewrite -addnS addKn -addnBA // mulnDl -{2}(addn1 i) -subn_sqr.
   rewrite addnBA ?leq_sqr // mulnS -addnA -mulnn -mulnDl.
   rewrite -(subnK (le_pmFp (vFp i) i)) mulnDl addnCA.
   rewrite -[1 ^ 2]/(Fp1 : nat) -addnBA // dvdn_addl.
     by rewrite Euclid_dvdM // -eqFp eq_sym orbC /dvdn Fp_mod eqn0Ngt lt0i.
-  by rewrite -eqn_mod_dvd // Fp_mod modnDl -(vFpV _ ni0) eqxx.
+  by rewrite -eqn_mod_dvd // Fp_mod modnDl -(vFpV _ ni0).
 suffices [mod_fact]: toFp (p.-1)`! = Fpn1.
   by rewrite /dvdn -addn1 -modnDml mod_fact addn1 prednK // modnn.
 rewrite dFact //; rewrite ((big_morph toFp) Fp1 mFpM) //; first last.
@@ -113,12 +112,11 @@ rewrite [mFpM _ _]mFp1 (bigD1 Fpn1) -?mFpA -/mFpM; last first.
   by rewrite [ltv _]ltn_neqAle vFpId eqxx orbT eq_sym eqF1n1.
 rewrite (reindex_onto vFp vFp) -/mFpM => [|i]; last by do 3!case/andP; auto.
 rewrite (eq_bigl (xpredD1 ltv Fp0)) => [|i]; last first.
-  rewrite andbC -!andbA -2!negb_or -vFpId orbC -leq_eqVlt.
-  rewrite andbA -ltnNge; symmetry; have [->|ni0] := eqVneq.
-    by case: eqP => // E; rewrite ?E !andbF.
-  by rewrite vFpK //eqxx vFp0.
+  rewrite andbC -!andbA -2!negb_or -vFpId orbC -leq_eqVlt -ltnNge.
+  have [->|ni0] := eqVneq i; last by rewrite vFpK // eqxx vFp0.
+  by case: eqP => // ->; rewrite !andbF.
 rewrite -{2}[mFp]/mFpM -[mFpM _ _]big_split -/mFpM.
-by rewrite big1 ?mFp1r //= => i /andP[]; auto.
+by rewrite big1 ?mFp1r //= => i /andP [/vFpV].
 Qed.
 
 (** The falling factorial *)
@@ -326,7 +324,7 @@ Qed.
 
 Lemma predn_exp m k : (m ^ k).-1 = m.-1 * (\sum_(i < k) m ^ i).
 Proof.
-rewrite -!subn1 -{1}(exp1n k) subn_exp; congr (_ * _).
+rewrite -!subn1 -[in LHS](exp1n k) subn_exp; congr (_ * _).
 symmetry; rewrite (reindex_inj rev_ord_inj); apply: eq_bigr => i _ /=.
 by rewrite -subn1 -subnDA exp1n muln1.
 Qed.
@@ -368,8 +366,7 @@ elim: n A => [|n IHn] A.
   by rewrite (@eq_card1 _ [tuple]) // => t; rewrite [t]tuple0 inE.
 rewrite -sum1dep_card (partition_big (@thead _ _) A) /= => [|t]; last first.
   by case/tupleP: t => x t; do 2!case/andP.
-transitivity (#|A| * #|A|.-1 ^_ n)%N; last by case: #|A|.
-rewrite -sum_nat_const; apply: eq_bigr => x Ax.
+rewrite ffactnS -sum_nat_const; apply: eq_bigr => x Ax.
 rewrite (cardD1 x) [x \in A]Ax /= -(IHn [predD1 A & x]) -sum1dep_card.
 rewrite (reindex (fun t : n.-tuple T => [tuple of x :: t])) /=; last first.
   pose ttail (t : n.+1.-tuple T) := [tuple of behead t].
@@ -428,7 +425,7 @@ rewrite (reindex (fun p : {ffun _} => [ffun i => f0 (p i)])) /=; last first.
   rewrite -im_f0 => /andP[/andP[/ffun_onP f_ffun /injectiveP injf] /eqP im_f].
   apply/ffunP=> i; rewrite !ffunE /ff0'; case: pickP => [y /eqP //|].
   have /imsetP[j _ eq_f0j_fi]: f i \in f0 @: 'I_k by rewrite -im_f mem_imset.
-  by move/(_ j)=> /eqP[].
+  by move/(_ j)/eqP.
 rewrite -ffactnn -card_inj_ffuns -sum1dep_card; apply: eq_bigl => p.
 rewrite -andbA.
 apply/and3P/injectiveP=> [[_ /injectiveP inj_f0p _] i j eq_pij | inj_p].
@@ -454,7 +451,7 @@ Proof.
 have [-> | n_gt0] := posnP n; last pose i0 := Ordinal n_gt0.
   case: m => [|m]; last by apply: eq_card0; case/tupleP=> [[]].
   by apply: (@eq_card1 _ [tuple]) => t; rewrite [t]tuple0 inE.
-rewrite -{12}[n]card_ord -card_draws.
+rewrite -[n in RHS]card_ord -card_draws.
 pose f_t (t : m.-tuple 'I_n) := [set i in t].
 pose f_A (A : {set 'I_n}) := [tuple of mkseq (nth i0 (enum A)) m].
 have val_fA (A : {set 'I_n}) : #|A| = m -> val (f_A A) = enum A.
@@ -465,13 +462,13 @@ have inc_A (A : {set 'I_n}) : sorted ltn (map val (enum A)).
   by rewrite (sorted_filter ltn_trans) // unlock val_ord_enum iota_ltn_sorted.
 rewrite -!sum1dep_card (reindex_onto f_t f_A) /= => [|A]; last first.
   by move/eqP=> cardAm; apply/setP=> x; rewrite inE -(mem_enum (mem A)) -val_fA.
-apply: eq_bigl => t; apply/idP/idP=> [inc_t|]; last first.
-  by case/andP; move/eqP=> t_m; move/eqP=> <-; rewrite val_fA.
+apply: eq_bigl => t.
+apply/idP/idP => [inc_t|/andP [/eqP t_m /eqP <-]]; last by rewrite val_fA.
 have ft_m: #|f_t t| = m.
   rewrite cardsE (card_uniqP _) ?size_tuple // -(map_inj_uniq val_inj).
   exact: (sorted_uniq ltn_trans ltnn).
 rewrite ft_m eqxx -val_eqE val_fA // -(inj_eq (inj_map val_inj)) /=.
-apply/eqP; apply: (eq_sorted_irr ltn_trans ltnn) => // y.
+apply/eqP/(eq_sorted_irr ltn_trans ltnn) => // y.
 by apply/mapP/mapP=> [] [x t_x ->]; exists x; rewrite // mem_enum inE in t_x *.
 Qed.
 
@@ -488,11 +485,11 @@ have add_mnC t: val \o add_mn t =1 add_mn_nat t \o val.
 pose f_add t := [tuple of map (add_mn t) (ord_tuple m)].
 rewrite -card_ltn_sorted_tuples -!sum1dep_card (reindex f_add) /=.
   apply: eq_bigl => t; rewrite -map_comp (eq_map (add_mnC t)) map_comp.
-  rewrite enumT unlock val_ord_enum -{1}(drop0 t).
+  rewrite enumT unlock val_ord_enum -[in LHS](drop0 t).
   have [m0 | m_gt0] := posnP m.
     by rewrite {2}m0 /= drop_oversize // size_tuple m0.
   have def_m := subnK m_gt0; rewrite -{2}def_m addn1 /= {1}/add_mn_nat.
-  move: 0 (m - 1) def_m => i k; rewrite -{1}(size_tuple t) => def_m.
+  move: 0 (m - 1) def_m => i k; rewrite -[in RHS](size_tuple t) => def_m.
   rewrite (drop_nth x0) /=; last by rewrite -def_m leq_addl.
   elim: k i (nth x0 t i) def_m => [|k IHk] i x /=.
     by rewrite add0n => ->; rewrite drop_size.
diff --git a/mathcomp/ssreflect/choice.v b/mathcomp/ssreflect/choice.v
index 4d7843c7d7..c065cd6496 100644
--- a/mathcomp/ssreflect/choice.v
+++ b/mathcomp/ssreflect/choice.v
@@ -82,7 +82,7 @@ Definition decode n := if n is 0 then [::] else [rec 0, n.-1, n.-1].
 Lemma decodeK : cancel decode code.
 Proof.
 have m2s: forall n, n.*2 - n = n by move=> n; rewrite -addnn addnK.
-case=> //= n; rewrite -[n.+1]mul1n -(expn0 2) -{3}[n]m2s.
+case=> //= n; rewrite -[n.+1]mul1n -(expn0 2) -[n in RHS]m2s.
 elim: n {2 4}n {1 3}0 => [|q IHq] [|[|r]] v //=; rewrite {}IHq ?mul1n ?m2s //.
 by rewrite expnSr -mulnA mul2n.
 Qed.
@@ -336,10 +336,9 @@ Lemma eq_xchoose P Q exP exQ : P =1 Q -> @xchoose P exP = @xchoose Q exQ.
 Proof.
 rewrite /xchoose => eqPQ.
 case: (xchoose_subproof exP) => x; case: (xchoose_subproof exQ) => y /=.
-case: ex_minnP => n; case: ex_minnP => m.
-rewrite -(extensional eqPQ) {1}(extensional eqPQ).
-move=> Qm minPm Pn minQn; suffices /eqP->: m == n by move=> -> [].
-by rewrite eqn_leq minQn ?minPm.
+case: ex_minnP => n; rewrite -(extensional eqPQ) => Pn minQn.
+case: ex_minnP => m; rewrite !(extensional eqPQ) => Qm minPm.
+by case: (eqVneq m n) => [-> -> [] //|]; rewrite eqn_leq minQn ?minPm.
 Qed.
 
 Lemma sigW P : (exists x, P x) -> {x | P x}.
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index 9047a4447f..17e3ac48b5 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -51,8 +51,8 @@ Proof.
 move=> lt_rd; have d_gt0: 0 < d by apply: leq_trans lt_rd.
 case: edivnP lt_rd => q' r'; rewrite d_gt0 /=.
 wlog: q q' r r' / q <= q' by case/orP: (leq_total q q'); last symmetry; eauto.
-rewrite leq_eqVlt; case/predU1P => [-> /addnI-> |] //=.
-rewrite -(leq_pmul2r d_gt0) => /leq_add lt_qr eq_qr _ /lt_qr {lt_qr}.
+have [||-> _ /addnI ->] //= := ltngtP q q'.
+rewrite -(leq_pmul2r d_gt0) => /leq_add lt_qr _ eq_qr _ /lt_qr {lt_qr}.
 by rewrite addnS ltnNge mulSn -addnA eq_qr addnCA addnA leq_addr.
 Qed.
 
@@ -189,7 +189,7 @@ rewrite {}/offset; case: d => // d _; rewrite /divn !modn_def.
 case: (edivnP m d.+1) (edivnP n d.+1) => [/= q r -> r_lt] [/= p s -> s_lt].
 rewrite addnACA -mulnDl; have [r_le s_le] := (ltnW r_lt, ltnW s_lt).
 have [d_ge|d_lt] := leqP; first by rewrite addn0 mul0n subn0 edivn_eq.
-rewrite addn1 mul1n -{1}(subnKC d_lt) addnA -mulSnr edivn_eq//.
+rewrite addn1 mul1n -[in LHS](subnKC d_lt) addnA -mulSnr edivn_eq//.
 by rewrite ltn_subLR// -addnS leq_add.
 Qed.
 
@@ -256,8 +256,8 @@ Proof. by case: d => // d; apply: modn_small; rewrite ltn_mod. Qed.
 
 Lemma modnMDl p m d : p * d + m = m %[mod d].
 Proof.
-case: (posnP d) => [-> | d_gt0]; first by rewrite muln0.
-by rewrite {1}(divn_eq m d) addnA -mulnDl modn_def edivn_eq // ltn_mod.
+have [->|d_gt0] := posnP d; first by rewrite muln0.
+by rewrite [in LHS](divn_eq m d) addnA -mulnDl modn_def edivn_eq // ltn_mod.
 Qed.
 
 Lemma muln_modr p m d : p * (m %% d) = (p * m) %% (p * d).
@@ -278,19 +278,16 @@ by rewrite mulSnr -addnS leq_add ?leq_mul2r.
 Qed.
 
 Lemma modnDl m d : d + m = m %[mod d].
-Proof. by rewrite -{1}[d]mul1n modnMDl. Qed.
+Proof. by rewrite -[m %% _](modnMDl 1) mul1n. Qed.
 
-Lemma modnDr m d : m + d = m %[mod d].
-Proof. by rewrite addnC modnDl. Qed.
+Lemma modnDr m d : m + d = m %[mod d]. Proof. by rewrite addnC modnDl. Qed.
 
-Lemma modnn d : d %% d = 0.
-Proof. by rewrite -[d in d %% _]addn0 modnDl mod0n. Qed.
+Lemma modnn d : d %% d = 0. Proof. by rewrite [d %% d](modnDr 0) mod0n. Qed.
 
 Lemma modnMl p d : p * d %% d = 0.
 Proof. by rewrite -[p * d]addn0 modnMDl mod0n. Qed.
 
-Lemma modnMr p d : d * p %% d = 0.
-Proof. by rewrite mulnC modnMl. Qed.
+Lemma modnMr p d : d * p %% d = 0. Proof. by rewrite mulnC modnMl. Qed.
 
 Lemma modnDml m n d : m %% d + n = m + n %[mod d].
 Proof. by rewrite [in RHS](divn_eq m d) -addnA modnMDl. Qed.
@@ -298,7 +295,7 @@ Proof. by rewrite [in RHS](divn_eq m d) -addnA modnMDl. Qed.
 Lemma modnDmr m n d : m + n %% d = m + n %[mod d].
 Proof. by rewrite !(addnC m) modnDml. Qed.
 
-Lemma modnDm m n d : m %% d  + n %% d = m + n %[mod d].
+Lemma modnDm m n d : m %% d + n %% d = m + n %[mod d].
 Proof. by rewrite modnDml modnDmr. Qed.
 
 Lemma eqn_modDl p m n d : (p + m == p + n %[mod d]) = (m == n %[mod d]).
@@ -333,9 +330,7 @@ by move=> d_even; rewrite [in RHS](divn_eq m d) oddD odd_mul d_even andbF.
 Qed.
 
 Lemma modnXm m n a : (a %% n) ^ m = a ^ m %[mod n].
-Proof.
-by elim: m => // m IHm; rewrite !expnS -modnMmr IHm modnMml modnMmr.
-Qed.
+Proof. by elim: m => // m IHm; rewrite !expnS -modnMmr IHm modnMml modnMmr. Qed.
 
 (** Divisibility **)
 
@@ -393,9 +388,7 @@ Lemma dvdn2 n : (2 %| n) = ~~ odd n.
 Proof. by rewrite /dvdn modn2; case (odd n). Qed.
 
 Lemma dvdn_odd m n : m %| n -> odd n -> odd m.
-Proof.
-by move=> m_dv_n; apply: contraTT; rewrite -!dvdn2 => /dvdn_trans->.
-Qed.
+Proof. by move=> m_dv_n; apply: contraTT; rewrite -!dvdn2 => /dvdn_trans->. Qed.
 
 Lemma divnK d m : d %| m -> m %/ d * d = m.
 Proof. by rewrite dvdn_eq; move/eqP. Qed.
@@ -440,8 +433,8 @@ Proof. by move=> n_gt0 lt_nd; rewrite /dvdn eqn0Ngt modn_small ?n_gt0. Qed.
 
 Lemma eqn_dvd m n : (m == n) = (m %| n) && (n %| m).
 Proof.
-case: m n => [|m] [|n] //; apply/idP/andP; first by move/eqP->; auto.
-rewrite eqn_leq => [[Hmn Hnm]]; apply/andP; have:= dvdn_leq; auto.
+case: m n => [|m] [|n] //; apply/idP/andP => [/eqP -> //| []].
+by rewrite eqn_leq => Hmn Hnm; do 2 rewrite dvdn_leq //.
 Qed.
 
 Lemma dvdn_pmul2l p d m : 0 < p -> (p * d %| p * m) = (d %| m).
@@ -507,8 +500,8 @@ Proof. by case: k => // k _ d_dv_m; rewrite expnS dvdn_mulr. Qed.
 
 Lemma dvdn_fact m n : 0 < m <= n -> m %| n`!.
 Proof.
-case: m => //= m; elim: n => //= n IHn; rewrite ltnS leq_eqVlt.
-by case/predU1P=> [-> | /IHn]; [apply: dvdn_mulr | apply: dvdn_mull].
+case: m => //= m; elim: n => //= n IHn; rewrite ltnS.
+have [/IHn/dvdn_mull->||-> _] // := ltngtP m n; exact: dvdn_mulr.
 Qed.
 
 Hint Resolve dvdn_add dvdn_sub dvdn_exp : core.
@@ -567,7 +560,7 @@ Proof.
 rewrite -subn1; case: d m => [|[|d]] [|m]//= _ _.
   by rewrite ?modn1 ?dvd1n ?modn0 ?subn1.
 rewrite modnB// (@modn_small 1)// [_ < _]leqn0 /dvdn mulnbl/= subn1.
-by case: ifP => // /eqP->; rewrite addn0.
+by case: eqP => // ->; rewrite addn0.
 Qed.
 
 Lemma edivn_pred m d : d != 1 -> 0 < m ->
@@ -601,8 +594,7 @@ Proof. by case=> // n; rewrite gcdnE modnn. Qed.
 
 Lemma gcdnC : commutative gcdn.
 Proof.
-move=> m n; wlog lt_nm: m n / n < m.
-  by case: (ltngtP n m) => [||-> //]; last symmetry; auto.
+move=> m n; wlog lt_nm: m n / n < m by have [? ->|? <-|-> //] := ltngtP n m.
 by rewrite gcdnE -[in m == 0](ltn_predK lt_nm) modn_small.
 Qed.
 
@@ -719,9 +711,9 @@ have m_gt0: 0 < m by rewrite addn_gt0 r_gt0 orbT.
 have d_gt0: 0 < d by rewrite gcdn_gt0 m_gt0.
 move/IHq=> {IHq} IHq le_kn_r le_kr_n def_d; apply: IHq => //; rewrite -/d.
   by rewrite mulnDl leq_add // -mulnA leq_mul2l le_kr_n orbT.
-apply: (@addIn d); rewrite -!addnA addnn addnCA mulnDr -addnA addnCA.
-rewrite /km mulnDl mulnCA mulnA -addnA; congr (_ + _).
-by rewrite -def_d addnC -addnA -mulnDl -mulnDr addn_negb -mul2n.
+apply: (@addIn d); rewrite mulnDr -addnA addnACA -def_d addnACA mulnA.
+rewrite -!mulnDl -mulnDr -addnA [kr * _]mulnC; congr addn.
+by rewrite addnC addn_negb muln1 mul2n addnn.
 Qed.
 
 Lemma Bezoutl m n : m > 0 -> {a | a < m & m %| gcdn m n + a * n}.
@@ -741,7 +733,7 @@ Lemma dvdn_gcd p m n : p %| gcdn m n = (p %| m) && (p %| n).
 Proof.
 apply/idP/andP=> [dv_pmn | [dv_pm dv_pn]].
   by rewrite !(dvdn_trans dv_pmn) ?dvdn_gcdl ?dvdn_gcdr.
-case (posnP n) => [->|n_gt0]; first by rewrite gcdn0.
+have [->|n_gt0] := posnP n; first by rewrite gcdn0.
 case: (Bezoutr m n_gt0) => // km _ /(dvdn_trans dv_pn).
 by rewrite dvdn_addl // dvdn_mull.
 Qed.
@@ -765,7 +757,7 @@ Proof. by move=> m n p q; rewrite -!gcdnA (gcdnCA n). Qed.
 
 Lemma muln_gcdr : right_distributive muln gcdn.
 Proof.
-move=> p m n; case: (posnP p) => [-> //| p_gt0].
+move=> p m n; have [-> //|p_gt0] := posnP p.
 elim/ltn_ind: m n => m IHm n; rewrite gcdnE [RHS]gcdnE muln_eq0 (gtn_eqF p_gt0).
 by case: posnP => // m_gt0; rewrite -muln_modr //=; apply/IHm/ltn_pmod.
 Qed.
@@ -988,7 +980,7 @@ Qed.
 Lemma dvdn_pexp2r m n k : k > 0 -> (m ^ k %| n ^ k) = (m %| n).
 Proof.
 move=> k_gt0; apply/idP/idP=> [dv_mn_k|]; last exact: dvdn_exp2r.
-case: (posnP n) => [-> | n_gt0]; first by rewrite dvdn0.
+have [->|n_gt0] := posnP n; first by rewrite dvdn0.
 have [n' def_n] := dvdnP (dvdn_gcdr m n); set d := gcdn m n in def_n.
 have [m' def_m] := dvdnP (dvdn_gcdl m n); rewrite -/d in def_m.
 have d_gt0: d > 0 by rewrite gcdn_gt0 n_gt0 orbT.
@@ -1013,7 +1005,7 @@ Lemma chinese_remainder x y :
   (x == y %[mod m1 * m2]) = (x == y %[mod m1]) && (x == y %[mod m2]).
 Proof.
 wlog le_yx : x y / y <= x; last by rewrite !eqn_mod_dvd // Gauss_dvd.
-by case/orP: (leq_total y x); last rewrite !(eq_sym (x %% _)); auto.
+by have [?|/ltnW ?] := leqP y x; last rewrite !(eq_sym (x %% _)); apply.
 Qed.
 
 (***********************************************************************)
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 12b060129c..bd58e010b4 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -409,7 +409,7 @@ Lemma bij_eq : bijective f -> forall x y, (f x == f y) = (x == y).
 Proof. by move/bij_inj; apply: inj_eq. Qed.
 
 Lemma can2_eq : cancel f g -> cancel g f -> forall x y, (f x == y) = (x == g y).
-Proof. by move=> fK gK x y; rewrite -{1}[y]gK; apply: can_eq. Qed.
+Proof. by move=> fK gK x y; rewrite -[y in LHS]gK; apply: can_eq. Qed.
 
 Lemma inj_in_eq :
   {in D &, injective f} -> {in D &, forall x y, (f x == f y) = (x == y)}.
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index 09ca95f85c..9fb79a2d67 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -413,7 +413,7 @@ Lemma orbit_uniq x : uniq (orbit x).
 Proof.
 rewrite /orbit -orderSpred looping_uniq; set n := (order x).-1.
 apply: contraFN (ltnn n) => /trajectP[i lt_i_n eq_fnx_fix].
-rewrite {1}/n orderSpred /order -(size_traject f x n).
+rewrite orderSpred -(size_traject f x n).
 apply: (leq_trans (subset_leq_card _) (card_size _)); apply/subsetP=> z.
 rewrite inE fconnect_orbit => /trajectP[j le_jn ->{z}].
 rewrite -orderSpred -/n ltnS leq_eqVlt in le_jn.
@@ -440,10 +440,7 @@ Lemma findex0 x : findex x x = 0.
 Proof. by rewrite /findex /orbit -orderSpred /= eqxx. Qed.
 
 Lemma findex_eq0 x y : (findex x y == 0) = (x == y).
-Proof.
-apply/idP/idP; last by move=> /eqP ->; rewrite findex0.
-by rewrite /findex /orbit -orderSpred /=; case: (x == y).
-Qed.
+Proof. by rewrite /findex /orbit -orderSpred /=; case: (x == y). Qed.
 
 Lemma fconnect_invariant (T' : eqType) (k : T -> T') :
   invariant f k =1 xpredT -> forall x y, fconnect f x y -> k x = k y.
@@ -491,8 +488,8 @@ Proof.
 suff Sf : {in S &, forall x y, fconnect f x y -> fconnect f y x}.
   by move=> *; apply/idP/idP=> /Sf->.
 move=> x _ xS _ /connectP [p f_p ->]; elim: p => //= y p IHp in x xS f_p *.
-move: f_p; rewrite -{2}(finv_f_in xS) => /andP[/eqP <- /(IHp _ (f_in xS))].
-by move=> /connect_trans -> //; apply: fconnect_finv.
+case/andP: f_p => /eqP <- /(IHp _ (f_in xS)) /connect_trans -> //.
+by apply: (connect_trans (fconnect_finv _)); rewrite finv_f_in.
 Qed.
 
 Lemma iter_order_in : {in S, forall x, iter (order x) f x = x}.
@@ -501,8 +498,8 @@ Proof. by move=> x xS; rewrite -orderSpred iterS; apply: f_finv_in. Qed.
 Lemma iter_finv_in n :
   {in S, forall x, n <= order x -> iter n finv x = iter (order x - n) f x}.
 Proof.
-move=> x xS; rewrite -{2}[x]iter_order_in => // /subnKC {1}<-; move: (_ - n).
-move=> m; rewrite iter_add; elim: n => // n {2}<-.
+move=> x xS; rewrite -[x in LHS]iter_order_in => // /subnKC {1}<-.
+move: (_ - n) => m; rewrite iter_add; elim: n => // n {2}<-.
 by rewrite iterSr /= finv_f_in // -iter_add iter_in.
 Qed.
 
@@ -586,9 +583,9 @@ Lemma fcard_order_set n (a : {pred T}) :
   a \subset order_set n -> fclosed f a -> fcard f a * n = #|a|.
 Proof.
 move=> a_n cl_a; rewrite /n_comp_mem; set b := [predI froots f & a].
-symmetry; transitivity #|preim (froot f) b|.
+suff <-: #|preim (froot f) b| = #|b| * n.
   apply: eq_card => x; rewrite !inE (roots_root fconnect_sym).
-  by rewrite -(closed_connect cl_a (connect_root _ x)).
+  exact/esym/(closed_connect cl_a)/connect_root.
 have{cl_a a_n} (x): b x -> froot f x = x /\ order x = n.
   by case/andP=> /eqP-> /(subsetP a_n)/eqnP->.
 elim: {a b}#|b| {1 3 4}b (eqxx #|b|) => [|m IHm] b def_m f_b.
@@ -705,7 +702,7 @@ Lemma fcycle_consEflatten : exists k, x :: p = flatten (nseq k.+1 (orbit x)).
 Proof.
 move: f_p; rewrite fcycle_consE; elim/ltn_ind: (size p) => n IHn t_cycle.
 have := order_le_cycle t_cycle (mem_head _ _); rewrite size_traject.
-case: ltngtP => //; last by move<-; exists 0; rewrite /= cats0.
+case: ltngtP => [||<-] //; last by exists 0; rewrite /= cats0.
 rewrite ltnS => n_ge _; have := t_cycle.
 rewrite -(subnKC n_ge) -addnS trajectD.
 rewrite (iter_order_in (mem_fcycle f_p) (inj_cycle f_p)) ?mem_head//.
@@ -750,9 +747,7 @@ by move=> x y xp yp; rewrite (orbitE fcycle_undup)// ?mem_rot ?mem_undup.
 Qed.
 
 Lemma eq_order_cycle : {in p &, forall x y, order y = order x}.
-Proof.
-by move=> x y xp yp; rewrite !(order_cycle fcycle_undup) ?mem_undup.
-Qed.
+Proof. by move=> x y xp yp; rewrite !(order_cycle fcycle_undup) ?mem_undup. Qed.
 
 Lemma iter_order_cycle : {in p &, forall x y, iter (order x) f y = y}.
 Proof.
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 9953c0de23..e608d2b272 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -900,7 +900,7 @@ Lemma subDset A B C : (A :\: B \subset C) = (A \subset B :|: C).
 Proof.
 apply/subsetP/subsetP=> sABC x; rewrite !inE.
   by case Bx: (x \in B) => // Ax; rewrite sABC ?inE ?Bx.
-by case Bx: (x \in B) => //; move/sABC; rewrite inE Bx.
+by case Bx: (x \in B) => // /sABC; rewrite inE Bx.
 Qed.
 
 Lemma subsetDP A B C :
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 432c30fa86..67f88a6ac6 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -737,9 +737,7 @@ Proof. by []. Qed.
 
 Lemma properP A B :
   reflect (A \subset B /\ (exists2 x, x \in B & x \notin A)) (A \proper B).
-Proof.
-by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn].
-Qed.
+Proof. by rewrite properE; apply: (iffP andP) => [] [-> /subsetPn]. Qed.
 
 Lemma proper_sub A B : A \proper B -> A \subset B.
 Proof. by case/andP. Qed.
@@ -1440,7 +1438,7 @@ Definition option_finMixin := Eval hnf in FinMixin option_enumP.
 Canonical option_finType := Eval hnf in FinType (option T) option_finMixin.
 
 Lemma card_option : #|{: option T}| = #|T|.+1.
-Proof. by rewrite !cardT !enumT {1}unlock /= !size_map. Qed.
+Proof. by rewrite !cardT !enumT [in LHS]unlock /= !size_map. Qed.
 
 End OptionFinType.
 
@@ -1714,7 +1712,7 @@ Proof. by apply: val_inj; apply: nth_enum_ord. Qed.
 
 Lemma index_enum_ord (i : 'I_n) : index i (enum 'I_n) = i.
 Proof.
-by rewrite -{1}(nth_ord_enum i i) index_uniq ?(enum_uniq, size_enum_ord).
+by rewrite -[in LHS](nth_ord_enum i i) index_uniq ?(enum_uniq, size_enum_ord).
 Qed.
 
 End OrdinalEnum.
@@ -2158,7 +2156,7 @@ Canonical tag_finType := Eval hnf in FinType {i : I & T_ i} tag_finMixin.
 Lemma card_tagged :
   #|{: {i : I & T_ i}}| = sumn (map (fun i => #|T_ i|) (enum I)).
 Proof.
-rewrite cardE !enumT {1}unlock size_flatten /shape -map_comp.
+rewrite cardE !enumT [in LHS]unlock size_flatten /shape -map_comp.
 by congr (sumn _); apply: eq_map => i; rewrite /= size_map -enumT -cardE.
 Qed.
 
@@ -2184,7 +2182,6 @@ Definition sum_finMixin := Eval hnf in UniqFinMixin sum_enum_uniq mem_sum_enum.
 Canonical sum_finType := Eval hnf in FinType (T1 + T2) sum_finMixin.
 
 Lemma card_sum : #|{: T1 + T2}| = #|T1| + #|T2|.
-Proof. by rewrite !cardT !enumT {1}unlock size_cat !size_map. Qed.
-
+Proof. by rewrite !cardT !enumT [in LHS]unlock size_cat !size_map. Qed.
 
 End SumFinType.
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index 4eeada91aa..5ec40372bd 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -482,7 +482,7 @@ Lemma equiv_sym : symmetric e. Proof. by case: e => [] ? []. Qed.
 Lemma equiv_trans : transitive e. Proof. by case: e => [] ? []. Qed.
 
 Lemma eq_op_trans (T' : eqType) : transitive (@eq_op T').
-Proof. by move=> x y z; move/eqP->; move/eqP->. Qed.
+Proof. by move=> x y z /eqP -> /eqP ->. Qed.
 
 Lemma equiv_ltrans: left_transitive e.
 Proof. by apply: left_trans; [apply: equiv_sym|apply: equiv_trans]. Qed.
@@ -598,8 +598,7 @@ Definition pi := locked (fun x => EquivQuotient (canon_id x)).
 
 Lemma ereprK : cancel erepr pi.
 Proof.
-unlock pi; case=> x hx; move/eqP:(hx)=> hx'.
-exact: (@val_inj _ _ [subType for erepr]).
+by unlock pi; case=> x hx; apply/(@val_inj _ _ [subType for erepr])/eqP.
 Qed.
 
 Local Notation encDE := (encModRelE encD).
@@ -629,9 +628,7 @@ exact/pi_CD.
 Qed.
 
 Lemma equivQTP : cancel (CD \o erepr) (pi \o DC).
-Proof.
-by move=> x; rewrite /= (pi_CD _ (erepr x) _) ?ereprK /eC /= ?encDP.
-Qed.
+Proof. by move=> x; rewrite /= (pi_CD _ (erepr x) _) ?ereprK /eC /= ?encDP. Qed.
 
 Local Notation qT := (type_of (Phantom (rel D) encD)).
 Definition quotClass := QuotClass equivQTP.
diff --git a/mathcomp/ssreflect/path.v b/mathcomp/ssreflect/path.v
index 9327a2feaa..6e72af0ac6 100644
--- a/mathcomp/ssreflect/path.v
+++ b/mathcomp/ssreflect/path.v
@@ -129,7 +129,7 @@ Proof. by case: p => //= x p; rewrite rcons_path andbC. Qed.
 Lemma rot_cycle p : cycle (rot n0 p) = cycle p.
 Proof.
 case: n0 p => [|n] [|y0 p] //=; first by rewrite /rot /= cats0.
-rewrite /rot /= -{3}(cat_take_drop n p) -cats1 -catA cat_path.
+rewrite /rot /= -[p in RHS](cat_take_drop n) -cats1 -catA cat_path.
 case: (drop n p) => [|z0 q]; rewrite /= -cats1 !cat_path /= !andbT andbC //.
 by rewrite last_cat; repeat bool_congr.
 Qed.
@@ -1167,14 +1167,14 @@ Qed.
 Lemma cycle_from_next : (forall x, x \in p -> e x (next p x)) -> cycle e p.
 Proof.
 case: p (next p) cycle_next => //= [x q] n; rewrite -(belast_rcons x q x).
-move: {q}(rcons q x) => q n_q; move/allP.
+move: {q}(rcons q x) => q n_q /allP.
 by elim: q x n_q => //= _ q IHq x /andP[/eqP <- n_q] /andP[-> /IHq->].
 Qed.
 
 Lemma cycle_from_prev : (forall x, x \in p -> e (prev p x) x) -> cycle e p.
 Proof.
-move=> e_p; apply: cycle_from_next => x p_x.
-by rewrite -{1}[x]prev_next e_p ?mem_next.
+move=> e_p; apply: cycle_from_next => x.
+by rewrite -mem_next => /e_p; rewrite prev_next.
 Qed.
 
 Lemma next_rot : next (rot n0 p) =1 next p.
@@ -1221,7 +1221,7 @@ by case: q => // y q; rewrite !rev_cons !(=^~ rcons_cons, rotr1_rcons) /= eqxx.
 Qed.
 
 Lemma next_rev p : uniq p -> next (rev p) =1 prev p.
-Proof. by move=> Up x; rewrite -{2}[p]revK prev_rev // rev_uniq. Qed.
+Proof. by move=> Up x; rewrite -[p in RHS]revK prev_rev // rev_uniq. Qed.
 
 End UniqCycleRev.
 
@@ -1246,7 +1246,7 @@ Variables (T T' : eqType) (h : T' -> T) (e : rel T) (e' : rel T').
 Hypothesis Ih : injective h.
 
 Lemma mem2_map x' y' p' : mem2 (map h p') (h x') (h y') = mem2 p' x' y'.
-Proof. by rewrite {1}/mem2 (index_map Ih) -map_drop mem_map. Qed.
+Proof. by rewrite [LHS]/mem2 (index_map Ih) -map_drop mem_map. Qed.
 
 Lemma next_map p : uniq p -> forall x, next (map h p) (h x) = h (next p x).
 Proof.
@@ -1259,7 +1259,7 @@ Qed.
 
 Lemma prev_map p : uniq p -> forall x, prev (map h p) (h x) = h (prev p x).
 Proof.
-move=> Up x; rewrite -{1}[x](next_prev Up) -(next_map Up).
+move=> Up x; rewrite -[x in LHS](next_prev Up) -(next_map Up).
 by rewrite prev_next ?map_inj_uniq.
 Qed.
 
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 02d3cdad04..2f35e35ea7 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -82,11 +82,11 @@ Variant elogn2_spec n : nat * nat -> Type :=
 
 Lemma elogn2P n : elogn2_spec n.+1 (elogn2 0 n n).
 Proof.
-rewrite -{1}[n.+1]mul1n -[1]/(2 ^ 0) -{1}(addKn n n) addnn.
+rewrite -[n.+1]mul1n -[1]/(2 ^ 0) -[n in _ * n.+1](addKn n n) addnn.
 elim: n {1 4 6}n {2 3}0 (leqnn n) => [|q IHq] [|[|r]] e //=; last first.
   by move/ltnW; apply: IHq.
-clear 1; rewrite subn1 -[_.-1.+1]doubleS -mul2n mulnA -expnSr.
-by rewrite -{1}(addKn q q) addnn; apply: IHq.
+rewrite subn1 prednK // -mul2n mulnA -expnSr.
+by rewrite -[q in _ * q.+1](addKn q q) addnn => _; apply: IHq.
 Qed.
 
 Definition ifnz T n (x y : T) := if n is 0 then y else x.
@@ -217,7 +217,7 @@ have lt1p: 1 < p by rewrite ltnS double_gt0.
 have co_p_2: coprime p 2 by rewrite /coprime gcdnC gcdnE modn2 /= odd_double.
 have if_d0: d = 0 -> [/\ m = (p + a.*2) * p, lb_dvd p p & lb_dvd p (p + a.*2)].
   move=> d0; have{d0 def_m} def_m: m = (p + a.*2) * p.
-    by rewrite d0 addn0 -mulnn -!mul2n mulnA -mulnDl in def_m *.
+    by rewrite d0 addn0 -!mul2n mulnA -mulnDl in def_m *.
   split=> //; apply/hasPn=> r /(hasPn leppm); apply: contra => /= dv_r.
     by rewrite def_m dvdn_mull.
   by rewrite def_m dvdn_mulr.
@@ -267,18 +267,17 @@ case def_d: d if_d0 => [|d'] => [[//|{def_m ltdp pr_p} def_m pr_p pr_m'] | _].
     rewrite lt0k -addn1 leq_add2l {1}def_a pr_m' pr_p /= def_k1 -addnn.
     by rewrite leq_addr.
   rewrite -addnA -doubleD addnCA def_a addSnnS def_k1 -(addnC k) -mulnSr.
-  rewrite -[_.*2.+1]/p mulnDl doubleD addnA -mul2n mulnA mul2n -mulSn.
-  by rewrite -/p mulnn.
+  by rewrite -[_.*2.+1]/p mulnDl doubleD addnA -mul2n mulnA mul2n -mulSn.
 have next_pm: lb_dvd p.+2 m.
   rewrite /lb_dvd /index_iota 2!subSS subn0 -(subnK lt1p) iota_add.
   rewrite has_cat; apply/norP; split=> //=; rewrite orbF subnKC // orbC.
   apply/norP; split; apply/dvdnP=> [[q def_q]].
      case/hasP: leppm; exists 2; first by rewrite /p -(subnKC lt0k).
     by rewrite /= def_q dvdn_mull // dvdn2 /= odd_double.
-  move/(congr1 (dvdn p)): def_m; rewrite -mulnn -!mul2n mulnA -mulnDl.
+  move/(congr1 (dvdn p)): def_m; rewrite -!mul2n mulnA -mulnDl.
   rewrite dvdn_mull // dvdn_addr; last by rewrite def_q dvdn_mull.
   case/dvdnP=> r; rewrite mul2n => def_r; move: ltdp (congr1 odd def_r).
-  rewrite odd_double -ltn_double {1}def_r -mul2n ltn_pmul2r //.
+  rewrite odd_double -ltn_double def_r -mul2n ltn_pmul2r //.
   by case: r def_r => [|[|[]]] //; rewrite def_d // mul1n /= odd_double.
 apply: apd_ok => //; case: a' def_a le_a_n => [|a'] def_a => [_ | lta] /=.
   rewrite /pd_ok /= /pfactor expn1 muln1 /pd_ord /= ltpm /pf_ok !andbT /=.
@@ -290,8 +289,8 @@ apply: apd_ok => //; case: a' def_a le_a_n => [|a'] def_a => [_ | lta] /=.
   rewrite mem_index_iota -(ltn_pmul2r (ltnW lt1q)) -def_r mul1n ltqm /=.
   rewrite -(@ltn_pmul2l p.+2) //; apply: (@leq_ltn_trans m).
     by rewrite def_r mulnC leq_mul.
-  rewrite -addn2 mulnn sqrnD mul2n muln2 -addnn addnCA -addnA addnCA addnA.
-  by rewrite def_a mul1n in def_m; rewrite -def_m addnS -addnA ltnS leq_addr.
+  rewrite -addn2 mulnn sqrnD mul2n muln2 -addnn addnACA.
+  by rewrite def_a mul1n in def_m; rewrite -def_m addnS /= ltnS -addnA leq_addr.
 set bc := ifnz _ _ _; apply: leq_pd_ok (leqnSn _) _.
 rewrite -doubleS -{1}[m]mul1n -[1]/(k.+1.*2.+1 ^ 0)%N.
 apply: IHn; first exact: ltnW.
@@ -299,7 +298,7 @@ rewrite doubleS -/p [ifnz 0 _ _]/=; do 2?split => //.
   rewrite orbT next_pm /= -(leq_add2r d.*2) def_m 2!addSnnS -doubleS leq_add.
   - move: ltc; rewrite /kb {}/bc andbT; case e => //= e' _; case: ifnzP => //.
     by case: edivn2P.
-  - by rewrite -{1}[p]muln1 -mulnn ltn_pmul2l.
+  - by rewrite -[p in p < _]muln1 ltn_pmul2l.
   by rewrite leq_double def_a mulSn (leq_trans ltdp) ?leq_addr.
 rewrite mulnDl !muln2 -addnA addnCA doubleD addnCA.
 rewrite (_ : _ + bc.2 = d); last first.
@@ -320,14 +319,14 @@ case: prime_decomp => [|[q [|[|e]]] pd] //=; last first; last by rewrite andbF.
   rewrite {1}/pfactor 2!expnS -!mulnA /=.
   case: (_ ^ _ * _) => [|u -> _ /andP[lt1q _]]; first by rewrite !muln0.
   left; right; exists q; last by rewrite dvdn_mulr.
-  have lt0q := ltnW lt1q; rewrite lt1q -{1}[q]muln1 ltn_pmul2l //.
+  have lt0q := ltnW lt1q; rewrite lt1q -[q in q < _]muln1 ltn_pmul2l //.
   by rewrite -[2]muln1 leq_mul.
 rewrite {1}/pfactor expn1; case: pd => [|[r e] pd] /=; last first.
   case: e => [|e] /=; first by rewrite !andbF.
   rewrite {1}/pfactor expnS -mulnA.
   case: (_ ^ _ * _) => [|u -> _ /and3P[lt1q ltqr _]]; first by rewrite !muln0.
   left; right; exists q; last by rewrite dvdn_mulr.
-  by rewrite lt1q -{1}[q]mul1n ltn_mul // -[q.+1]muln1 leq_mul.
+  by rewrite lt1q -[q in q < _]mul1n ltn_mul // -[q.+1]muln1 leq_mul.
 rewrite muln1 !andbT => def_q pr_q lt1q; right=> [[]] // [d].
 by rewrite def_q -mem_index_iota => in_d_2q dv_d_q; case/hasP: pr_q; exists d.
 Qed.
@@ -435,11 +434,11 @@ Qed.
 
 Lemma mem_primes p n : (p \in primes n) = [&& prime p, n > 0 & p %| n].
 Proof.
-rewrite andbCA; case: posnP => [-> // | /= n_gt0].
+rewrite andbCA; have [-> // | /= n_gt0] := posnP.
 apply/mapP/andP=> [[[q e]]|[pr_p]] /=.
-  case/mem_prime_decomp=> pr_q e_gt0; case/dvdnP=> u -> -> {p}.
+  case/mem_prime_decomp=> pr_q e_gt0 /dvdnP [u ->] -> {p}.
   by rewrite -(prednK e_gt0) expnS mulnCA dvdn_mulr.
-rewrite {1}(prod_prime_decomp n_gt0) big_seq.
+rewrite [n in _ %| n]prod_prime_decomp // big_seq.
 apply big_ind => [| u v IHu IHv | [q e] /= mem_qe dv_p_qe].
 - by rewrite Euclid_dvd1.
 - by rewrite Euclid_dvdM // => /orP[].
@@ -474,9 +473,7 @@ Lemma pdiv_prime n : 1 < n -> prime (pdiv n).
 Proof. by rewrite -pi_pdiv mem_primes; case/and3P. Qed.
 
 Lemma pdiv_dvd n : pdiv n %| n.
-Proof.
-by case: n (pi_pdiv n) => [|[|n]] //; rewrite mem_primes=> /and3P[].
-Qed.
+Proof. by case: n (pi_pdiv n) => [|[|n]] //; rewrite mem_primes=> /and3P[]. Qed.
 
 Lemma pi_max_pdiv n : (max_pdiv n \in \pi(n)) = (n > 1).
 Proof.
@@ -507,13 +504,12 @@ Hint Resolve pdiv_gt0 max_pdiv_gt0 : core.
 
 Lemma pdiv_min_dvd m d : 1 < d -> d %| m -> pdiv m <= d.
 Proof.
-move=> lt1d dv_d_m; case: (posnP m) => [->|mpos]; first exact: ltnW.
+case: (posnP m) => [->|mpos] lt1d dv_d_m; first exact: ltnW.
 rewrite /pdiv; apply: leq_trans (pdiv_leq (ltnW lt1d)).
 have: pdiv d \in primes m.
   by rewrite mem_primes mpos pdiv_prime // (dvdn_trans (pdiv_dvd d)).
-case: (primes m) (sorted_primes m) => //= p pm ord_pm.
-rewrite inE => /predU1P[-> //|].
-by move/(allP (order_path_min ltn_trans ord_pm)); apply: ltnW.
+case: (primes m) (sorted_primes m) => //= p pm ord_pm; rewrite inE.
+by case/predU1P => [-> | /(allP (order_path_min ltn_trans ord_pm)) /ltnW].
 Qed.
 
 Lemma max_pdiv_max n p : p \in \pi(n) -> p <= max_pdiv n.
@@ -530,10 +526,9 @@ Proof.
 case def_n: n => [|[|n']] // _; rewrite -def_n => lt_n_p2.
 suffices ->: n = pdiv n by rewrite pdiv_prime ?def_n.
 apply/eqP; rewrite eqn_leq leqNgt andbC pdiv_leq; last by rewrite def_n.
-move: lt_n_p2; rewrite ltnNge; apply: contra => lt_pm_m.
-case/dvdnP: (pdiv_dvd n) => q def_q.
-rewrite {2}def_q -mulnn leq_pmul2r // pdiv_min_dvd //.
-  by rewrite -[pdiv n]mul1n {2}def_q ltn_pmul2r in lt_pm_m.
+apply/contraL: lt_n_p2 => lt_pm_m; case/dvdnP: (pdiv_dvd n) => q def_q.
+rewrite -leqNgt [n in _ <= n]def_q leq_pmul2r // pdiv_min_dvd //.
+  by rewrite -[pdiv n]mul1n [n in _ < n]def_q ltn_pmul2r in lt_pm_m.
 by rewrite def_q dvdn_mulr.
 Qed.
 
@@ -543,10 +538,10 @@ Proof.
 apply: (iffP idP) => [npr_p|]; last first.
   case=> [|[p [pr_p le_p2_n dv_p_n]]]; first by case: n => [|[]].
   apply/negP=> pr_n; move: dv_p_n le_p2_n; rewrite dvdn_prime2 //; move/eqP->.
-  by rewrite leqNgt -{1}[n]muln1 -mulnn ltn_pmul2l ?prime_gt1 ?prime_gt0.
-case: leqP => [lt1p|]; [right | by left].
+  by rewrite leqNgt -[n in n < _]muln1 ltn_pmul2l ?prime_gt1 ?prime_gt0.
+have [lt1p|] := leqP; [right | by left].
 exists (pdiv n); rewrite pdiv_dvd pdiv_prime //; split=> //.
-by case: leqP npr_p => //; move/ltn_pdiv2_prime->; auto.
+by case: leqP npr_p => // /ltn_pdiv2_prime -> //; exact: ltnW.
 Qed.
 
 Arguments primePns {n}.
@@ -563,7 +558,7 @@ Qed.
 
 Lemma primes_exp m n : n > 0 -> primes (m ^ n) = primes m.
 Proof.
-case: n => // n _; rewrite expnS; case: (posnP m) => [-> //| m_gt0].
+case: n => // n _; rewrite expnS; have [-> // | m_gt0] := posnP m.
 apply/eq_primes => /= p; elim: n => [|n IHn]; first by rewrite muln1.
 by rewrite primes_mul ?(expn_gt0, expnS, IHn, orbb, m_gt0).
 Qed.
@@ -723,7 +718,8 @@ Proof.
 case p_pr: (prime p); last by rewrite /logn p_pr.
 have xlp := pfactor_coprime p_pr.
 case/xlp=> m' co_m' def_m /xlp[n' co_n' def_n] {xlp}.
-by rewrite {1}def_m {1}def_n mulnCA -mulnA -expnD !logn_Gauss // pfactorK.
+rewrite [in LHS]def_m [in LHS]def_n mulnCA -mulnA -expnD !logn_Gauss //.
+exact: pfactorK.
 Qed.
 
 Lemma lognX p m n : logn p (m ^ n) = n * logn p m.
@@ -750,7 +746,7 @@ apply: (iffP idP) => [dv_d_pn|[m le_m_n ->]]; last first.
 exists (logn p d); first by rewrite -(pfactorK n p_pr) dvdn_leq_log.
 have d_gt0: d > 0 by apply: dvdn_gt0 dv_d_pn.
 case: (pfactor_coprime p_pr d_gt0) => q co_p_q def_d.
-rewrite {1}def_d ((q =P 1) _) ?mul1n // -dvdn1.
+rewrite [LHS]def_d ((q =P 1) _) ?mul1n // -dvdn1.
 suff: q %| p ^ n * 1 by rewrite Gauss_dvdr // coprime_sym coprime_expl.
 by rewrite muln1 (dvdn_trans _ dv_d_pn) // def_d dvdn_mulr.
 Qed.
@@ -782,7 +778,8 @@ Proof.
 have [-> | d_gt0] := posnP d; first by rewrite big_add1 divn0 big1.
 apply: (@addnI (d %| 0)); rewrite -(@big_ltn _ 0 _ 0 _ (dvdn d)) // big_mkord.
 rewrite (partition_big (fun i : 'I_n.+1 => inord (i %/ d)) 'I_(n %/ d).+1) //=.
-rewrite dvdn0 add1n -{1}[_.+1]card_ord -sum1_card; apply: eq_bigr => [[q ?] _].
+rewrite dvdn0 add1n -[_.+1 in LHS]card_ord -sum1_card.
+apply: eq_bigr => [[q ?] _].
 rewrite (bigD1 (inord (q * d))) /eq_op /= !inordK ?ltnS -?leq_divRL ?mulnK //.
 rewrite dvdn_mull ?big1 // => [[i /= ?] /andP[/eqP <- /negPf]].
 by rewrite eq_sym dvdn_eq inordK ?ltnS ?leq_div2r // => ->.
@@ -866,7 +863,7 @@ Proof. by move=> eq_pi n; rewrite 3!inE /= eq_pi. Qed.
 Lemma eq_piP m n : \pi(m) =i \pi(n) <-> \pi(m) = \pi(n).
 Proof.
 rewrite /pi_of; have eqs := eq_sorted_irr ltn_trans ltnn.
-by split=> [|-> //]; move/(eqs _ _ (sorted_primes m) (sorted_primes n)) ->.
+by split=> [|-> //] /(eqs _ _ (sorted_primes m) (sorted_primes n)) ->.
 Qed.
 
 Lemma part_gt0 pi n : 0 < n`_pi.
@@ -926,7 +923,7 @@ Qed.
 Lemma partnX pi m n : (m ^ n)`_pi = m`_pi ^ n.
 Proof.
 elim: n => [|n IHn]; first exact: partn1.
-rewrite expnS; case: (posnP m) => [->|m_gt0]; first by rewrite partn0 exp1n.
+rewrite expnS; have [->|m_gt0] := posnP m; first by rewrite partn0 exp1n.
 by rewrite expnS partnM ?IHn // expn_gt0 m_gt0.
 Qed.
 
@@ -939,7 +936,7 @@ Qed.
 Lemma p_part p n : n`_p = p ^ logn p n.
 Proof.
 case (posnP (logn p n)) => [log0 |].
-  by rewrite log0 [n`_p]big1_seq // => q; case/andP; move/eqnP->; rewrite log0.
+  by rewrite log0 [n`_p]big1_seq // => q /andP [/eqP ->]; rewrite log0.
 rewrite logn_gt0 mem_primes; case/and3P=> _ n_gt0 dv_p_n.
 have le_p_n: p < n.+1 by rewrite ltnS dvdn_leq.
 by rewrite [n`_p]big_mkord (big_pred1 (Ordinal le_p_n)).
@@ -982,13 +979,13 @@ Qed.
 
 Lemma partn_pi n : n > 0 -> n`_\pi(n) = n.
 Proof.
-move=> n_gt0; rewrite {3}(prod_prime_decomp n_gt0) prime_decompE big_map.
+move=> n_gt0; rewrite [RHS]prod_prime_decomp // prime_decompE big_map.
 by rewrite -[n`__]big_filter filter_pi_of.
 Qed.
 
 Lemma partnT n : n > 0 -> n`_predT = n.
 Proof.
-move=> n_gt0; rewrite -{2}(partn_pi n_gt0) {2}/partn big_mkcond /=.
+move=> n_gt0; rewrite -[RHS]partn_pi // [RHS]/partn big_mkcond /=.
 by apply: eq_bigr => p _; rewrite -logn_gt0; case: (logn p _).
 Qed.
 
@@ -999,7 +996,7 @@ Qed.
 
 Lemma partnC pi n : n > 0 -> n`_pi * n`_pi^' = n.
 Proof.
-move=> n_gt0; rewrite -{3}(partnT n_gt0) /partn.
+move=> n_gt0; rewrite -[RHS]partnT /partn //.
 do 2!rewrite mulnC big_mkcond /=; rewrite -big_split; apply: eq_bigr => p _ /=.
 by rewrite mulnC inE /=; case: (p \in pi); rewrite /= (muln1, mul1n).
 Qed.
@@ -1018,7 +1015,7 @@ Proof.
 move=> m_gt0 n_gt0; have p_gt0: lcmn m n > 0 by rewrite lcmn_gt0 m_gt0.
 apply/eqP; rewrite eqn_dvd dvdn_lcm !partn_dvd ?dvdn_lcml ?dvdn_lcmr //.
 rewrite -(dvdn_pmul2r (part_gt0 pi^' (lcmn m n))) partnC // dvdn_lcm !andbT.
-rewrite -{1}(partnC pi m_gt0) andbC -{1}(partnC pi n_gt0).
+rewrite -[m in m %| _](partnC pi m_gt0) andbC -[n in n %| _](partnC pi n_gt0).
 by rewrite !dvdn_mul ?partn_dvd ?dvdn_lcml ?dvdn_lcmr.
 Qed.
 
@@ -1027,7 +1024,7 @@ Proof.
 move=> m_gt0 n_gt0; have p_gt0: gcdn m n > 0 by rewrite gcdn_gt0 m_gt0.
 apply/eqP; rewrite eqn_dvd dvdn_gcd !partn_dvd ?dvdn_gcdl ?dvdn_gcdr //=.
 rewrite -(dvdn_pmul2r (part_gt0 pi^' (gcdn m n))) partnC // dvdn_gcd.
-rewrite -{3}(partnC pi m_gt0) andbC -{3}(partnC pi n_gt0).
+rewrite -[m in _ %| m](partnC pi m_gt0) andbC -[n in _%| n](partnC pi n_gt0).
 by rewrite !dvdn_mul ?partn_dvd ?dvdn_gcdl ?dvdn_gcdr.
 Qed.
 
@@ -1178,7 +1175,7 @@ Proof. by move=> pi'm pi_n; rewrite (pnat_coprime pi'm) ?pnatNK. Qed.
 Lemma sub_pnat_coprime pi rho m n :
   {subset rho <= pi^'} -> pi.-nat m -> rho.-nat n -> coprime m n.
 Proof.
-by move=> pi'rho pi_m; move/(sub_in_pnat (in1W pi'rho)); apply: pnat_coprime.
+by move=> pi'rho pi_m /(sub_in_pnat (in1W pi'rho)); apply: pnat_coprime.
 Qed.
 
 Lemma coprime_partC pi m n : coprime m`_pi n`_pi^'.
@@ -1191,9 +1188,8 @@ Qed.
 
 Lemma part_pnat_id pi n : pi.-nat n -> n`_pi = n.
 Proof.
-case/andP=> n_gt0 pi_n.
-rewrite -{2}(partnT n_gt0) /partn big_mkcond; apply: eq_bigr=> p _.
-have [->|] := posnP (logn p n); first by rewrite if_same.
+case/andP=> n_gt0 pi_n; rewrite -[RHS]partnT // /partn big_mkcond /=.
+apply: eq_bigr=> p _; have [->|] := posnP (logn p n); first by rewrite if_same.
 by rewrite logn_gt0 => /(allP pi_n)/= ->.
 Qed.
 
@@ -1229,8 +1225,7 @@ Proof. by move=> p_n; exists (logn p n); rewrite -p_part part_pnat_id. Qed.
 
 Lemma pi'_p'nat pi p n : pi^'.-nat n -> p \in pi -> p^'.-nat n.
 Proof.
-move=> pi'n pi_p; apply: sub_in_pnat pi'n => q _.
-by apply: contraNneq => ->.
+by move=> pi'n pi_p; apply: sub_in_pnat pi'n => q _; apply: contraNneq => ->.
 Qed.
  
 Lemma pi_p'nat p pi n : pi.-nat n -> p \in pi^' -> p^'.-nat n.
@@ -1239,7 +1234,7 @@ Proof. by move=> pi_n; apply: pi'_p'nat; rewrite pnatNK. Qed.
 Lemma partn_part pi rho n : {subset pi <= rho} -> n`_rho`_pi = n`_pi.
 Proof.
 move=> pi_sub_rho; have [->|n_gt0] := posnP n; first by rewrite !partn0 partn1.
-rewrite -{2}(partnC rho n_gt0) partnM //.
+rewrite -[in RHS](partnC rho n_gt0) partnM //.
 suffices: pi^'.-nat n`_rho^' by move/part_p'nat->; rewrite muln1.
 by apply: sub_in_pnat (part_pnat _ _) => q _; apply/contra/pi_sub_rho.
 Qed.
@@ -1346,7 +1341,7 @@ Lemma modn_partP n a b : 0 < n ->
 Proof.
 move=> n_gt0; wlog le_b_a: a b / b <= a.
   move=> IH; case: (leqP b a) => [|/ltnW] /IH {IH}// IH.
-  by rewrite eq_sym; apply: (iffP IH) => eqab p; move/eqab.
+  by rewrite eq_sym; apply: (iffP IH) => eqab p /eqab.
 rewrite eqn_mod_dvd //; apply: (iffP (dvdn_partP _ n_gt0)) => eqab p /eqab;
   by rewrite -eqn_mod_dvd // => /eqP.
 Qed.
@@ -1433,6 +1428,3 @@ rewrite -!big_mkcond -sum_nat_const pair_big (reindex_onto h h') => [|[d d'] _].
 apply/eqP; rewrite /eq_op /= /eq_op /= !modn_dvdm ?dvdn_part //.
 by rewrite chinese_modl // chinese_modr // !modn_small ?eqxx ?ltn_ord.
 Qed.
-
-
-
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index aca2b77c50..920f393f62 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -351,7 +351,7 @@ Lemma last_ind P :
 Proof.
 move=> Hnil Hlast s; rewrite -(cat0s s).
 elim: s [::] Hnil => [|x s2 IHs] s1 Hs1; first by rewrite cats0.
-by rewrite -cat_rcons; auto.
+by rewrite -cat_rcons; apply/IHs/Hlast.
 Qed.
 
 (* Sequence indexing. *)
@@ -433,8 +433,7 @@ 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.
-do 2!rewrite !nth_set_nth /=; case: eqP => // ->.
-by rewrite eq_sym -if_neg ne_n12.
+by do 2!rewrite !nth_set_nth /=; case: eqP => // ->; case: eqVneq ne_n12.
 Qed.
 
 (* find, count, has, all. *)
@@ -616,14 +615,12 @@ Proof. by rewrite -size_filter filter_predT. Qed.
 Lemma count_predUI a1 a2 s :
   count (predU a1 a2) s + count (predI a1 a2) s = count a1 s + count a2 s.
 Proof.
-elim: s => //= x s IHs; rewrite /= addnCA -addnA IHs addnA addnC.
-by rewrite -!addnA; do 2 nat_congr; case (a1 x); case (a2 x).
+elim: s => //= x s IHs; rewrite /= addnACA [RHS]addnACA IHs.
+by case: (a1 x) => //; rewrite addn0.
 Qed.
 
 Lemma count_predC a s : count a s + count (predC a) s = size s.
-Proof.
-by elim: s => //= x s IHs; rewrite addnCA -addnA IHs addnA addn_negb.
-Qed.
+Proof. by elim: s => //= x s IHs; rewrite addnACA IHs; case: (a _). Qed.
 
 Lemma count_filter a1 a2 s : count a1 (filter a2 s) = count (predI a1 a2) s.
 Proof. by rewrite -!size_filter filter_predI. Qed.
@@ -751,7 +748,7 @@ Qed.
 
 Lemma nth_drop s i : nth (drop n0 s) i = nth s (n0 + i).
 Proof.
-rewrite -{2}[s]cat_take_drop nth_cat size_take ltnNge.
+rewrite -[s in RHS]cat_take_drop nth_cat size_take ltnNge.
 case: ltnP => [?|le_s_n0]; rewrite ?(leq_trans le_s_n0) ?leq_addr ?addKn //=.
 by rewrite drop_oversize // !nth_default.
 Qed.
@@ -759,8 +756,8 @@ Qed.
 Lemma nth_take i : i < n0 -> forall s, nth (take n0 s) i = nth s i.
 Proof.
 move=> lt_i_n0 s; case lt_n0_s: (n0 < size s).
-  by rewrite -{2}[s]cat_take_drop nth_cat size_take lt_n0_s /= lt_i_n0.
-by rewrite -{1}[s]cats0 take_cat lt_n0_s /= cats0.
+  by rewrite -[s in RHS]cat_take_drop nth_cat size_take lt_n0_s /= lt_i_n0.
+by rewrite -[s in LHS]cats0 take_cat lt_n0_s /= cats0.
 Qed.
 
 Lemma take_take i j : i <= j -> forall s, take i (take j s) = take i s.
@@ -815,7 +812,7 @@ Lemma rot0 s : rot 0 s = s.
 Proof. by rewrite /rot drop0 take0 cats0. Qed.
 
 Lemma size_rot s : size (rot n0 s) = size s.
-Proof. by rewrite -{2}[s]cat_take_drop /rot !size_cat addnC. Qed.
+Proof. by rewrite -[s in RHS]cat_take_drop /rot !size_cat addnC. Qed.
 
 Lemma rot_oversize n s : size s <= n -> rot n s = s.
 Proof. by move=> le_s_n; rewrite /rot take_oversize ?drop_oversize. Qed.
@@ -989,7 +986,7 @@ Fixpoint eqseq s1 s2 {struct s2} :=
 Lemma eqseqP : Equality.axiom eqseq.
 Proof.
 move; elim=> [|x1 s1 IHs] [|x2 s2]; do [by constructor | simpl].
-case: (x1 =P x2) => [<-|neqx]; last by right; case.
+have [<-|neqx] := x1 =P x2; last by right; case.
 by apply: (iffP (IHs s2)) => [<-|[]].
 Qed.
 
@@ -1371,10 +1368,10 @@ by rewrite !inE (ltn_trans ltij ltjs) ltn_eqF //=; case.
 Qed.
 
 Lemma mem_rot s : rot n0 s =i s.
-Proof. by move=> x; rewrite -{2}(cat_take_drop n0 s) !mem_cat /= orbC. Qed.
+Proof. by move=> x; rewrite -[s in RHS](cat_take_drop n0) !mem_cat /= orbC. Qed.
 
 Lemma eqseq_rot s1 s2 : (rot n0 s1 == rot n0 s2) = (s1 == s2).
-Proof. by apply: inj_eq; apply: rot_inj. Qed.
+Proof. exact/inj_eq/rot_inj. Qed.
 
 End EqSeq.
 
@@ -1442,7 +1439,7 @@ Qed.
 End NthTheory.
 
 Lemma set_nth_default T s (y0 x0 : T) n : n < size s -> nth x0 s n = nth y0 s n.
-Proof. by elim: s n => [|y s' IHs] [|n] /=; auto. Qed.
+Proof. by elim: s n => [|y s' IHs] [|n] //= /IHs. Qed.
 
 Lemma headI T s (x : T) : rcons s x = head x s :: behead (rcons s x).
 Proof. by case: s. Qed.
@@ -1748,7 +1745,7 @@ Lemma rotrK : cancel (@rotr T n0) (rot n0).
 Proof.
 move=> s; have [lt_n0s | ge_n0s] := ltnP n0 (size s).
   by rewrite -{1}(subKn (ltnW lt_n0s)) -{1}[size s]size_rotr; apply: rotK.
-by rewrite -{2}(rot_oversize ge_n0s) /rotr (eqnP ge_n0s) rot0.
+by rewrite -[in RHS](rot_oversize ge_n0s) /rotr (eqnP ge_n0s) rot0.
 Qed.
 
 Lemma rotr_inj : injective (@rotr T n0).
@@ -1786,7 +1783,7 @@ Implicit Type s : seq T.
 
 Lemma rotD m n s : m + n <= size s -> rot (m + n) s = rot m (rot n s).
 Proof.
-move=> sz_s; rewrite {1}/rot -[take _ s](cat_take_drop n).
+move=> sz_s; rewrite [LHS]/rot -[take _ s](cat_take_drop n).
 rewrite 5!(catA, =^~ rot_size_cat) !cat_take_drop.
 by rewrite size_drop !size_takel ?leq_addl ?addnK.
 Qed.
@@ -1944,7 +1941,7 @@ exists (take i m ++ drop i.+1 m).
   rewrite size_cat size_take size_drop lt_i_m.
   by rewrite sz_m in lt_i_m *; rewrite subnKC.
 rewrite {s1 def_s1}[s1](congr1 behead def_s1).
-rewrite -[s2](cat_take_drop i) -{1}[m](cat_take_drop i) {}def_m_i -cat_cons.
+rewrite -[s2](cat_take_drop i) -[m in LHS](cat_take_drop i) {}def_m_i -cat_cons.
 have sz_i_s2: size (take i s2) = i by apply: size_takel; rewrite sz_m in lt_i_m.
 rewrite lastI cat_rcons !mask_cat ?size_nseq ?size_belast ?mask_false //=.
 by rewrite (drop_nth true) // nth_index -?index_mem.
@@ -1968,7 +1965,7 @@ Qed.
 Lemma cat_subseq s1 s2 s3 s4 :
   subseq s1 s3 -> subseq s2 s4 -> subseq (s1 ++ s2) (s3 ++ s4).
 Proof.
-case/subseqP=> m1 sz_m1 ->; case/subseqP=> m2 sz_m2 ->; apply/subseqP.
+case/subseqP=> m1 sz_m1 -> /subseqP [m2 sz_m2 ->]; apply/subseqP.
 by exists (m1 ++ m2); rewrite ?size_cat ?mask_cat ?sz_m1 ?sz_m2.
 Qed.
 
@@ -2133,9 +2130,7 @@ Lemma map_mask m s : map (mask m s) = mask m (map s).
 Proof. by elim: m s => [|[|] m IHm] [|x p] //=; rewrite IHm. Qed.
 
 Lemma inj_map : injective f -> injective map.
-Proof.
-by move=> injf; elim=> [|y1 s1 IHs] [|y2 s2] //= [/injf-> /IHs->].
-Qed.
+Proof. by move=> injf; elim=> [|y1 s1 IHs] [|y2 s2] //= [/injf-> /IHs->]. Qed.
 
 End Map.
 
@@ -2420,9 +2415,7 @@ Lemma size_iota m n : size (iota m n) = n.
 Proof. by elim: n m => //= n IHn m; rewrite IHn. Qed.
 
 Lemma iota_add m n1 n2 : iota m (n1 + n2) = iota m n1 ++ iota (m + n1) n2.
-Proof.
-by elim: n1 m => //= [|n1 IHn1] m; rewrite ?addn0 // -addSnnS -IHn1.
-Qed.
+Proof. by elim: n1 m => [|n1 IHn1] m; rewrite ?addn0 // -addSnnS /= -IHn1. Qed.
 
 Lemma iota_addl m1 m2 n : iota (m1 + m2) n = map (addn m1) (iota m2 n).
 Proof. by elim: n m2 => //= n IHn m2; rewrite -addnS IHn. Qed.
@@ -3176,7 +3169,7 @@ Lemma incr_tallyP x : {homo incr_tally^~ x : bs / bs \in wf_tally}.
 Proof.
 move=> bs /andP[]; rewrite unfold_in.
 elim: bs => [|[y [|n]] bs IHbs] //= /andP[bs'y Ubs]; rewrite inE /= => bs'0.
-rewrite eq_sym; case: ifP => [/eqP<- | y'x] /=; first by rewrite bs'y Ubs.
+have [<- | y'x] /= := eqVneq y; first by rewrite bs'y Ubs.
 rewrite -andbA {}IHbs {Ubs bs'0}// andbT.
 elim: bs bs'y => [|b bs IHbs] /=; rewrite inE ?y'x // => /norP[b'y bs'y].
 by case: ifP => _; rewrite /= inE negb_or ?y'x // b'y IHbs.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 505140859b..39c8451ee6 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -212,7 +212,7 @@ Lemma addnCA : left_commutative addn.
 Proof. by move=> m n p; elim: m => //= m; rewrite addnS => <-. Qed.
 
 Lemma addnC : commutative addn.
-Proof. by move=> m n; rewrite -{1}[n]addn0 addnCA addn0. Qed.
+Proof. by move=> m n; rewrite -[n in LHS]addn0 addnCA addn0. Qed.
 
 Lemma addn1 n : n + 1 = n.+1. Proof. by rewrite addnC. Qed.
 
@@ -273,11 +273,11 @@ Proof. by elim: p. Qed.
 Lemma subnDr p m n : (m + p) - (n + p) = m - n.
 Proof. by rewrite -!(addnC p) subnDl. Qed.
 
-Lemma addKn n : cancel (addn n) (subn^~ n).
-Proof. by move=> m; rewrite /= -{2}[n]addn0 subnDl subn0. Qed.
-
 Lemma addnK n : cancel (addn^~ n) (subn^~ n).
-Proof. by move=> m; rewrite /= (addnC m) addKn. Qed.
+Proof. by move=> m; rewrite (subnDr n m 0) subn0. Qed.
+
+Lemma addKn n : cancel (addn n) (subn^~ n).
+Proof. by move=> m; rewrite addnC addnK. Qed.
 
 Lemma subSnn n : n.+1 - n = 1.
 Proof. exact (addnK n 1). Qed.
@@ -493,18 +493,16 @@ Proof.
 by move=> le_mn1 le_mn2; rewrite (@leq_trans (m1 + n2)) ?leq_add2l ?leq_add2r.
 Qed.
 
-Lemma leq_addr m n : n <= n + m.
-Proof. by rewrite -{1}[n]addn0 leq_add2l. Qed.
+Lemma leq_addl m n : n <= m + n. Proof. exact: (leq_add2r n 0). Qed.
 
-Lemma leq_addl m n : n <= m + n.
-Proof. by rewrite addnC leq_addr. Qed.
-
-Lemma ltn_addr m n p : m < n -> m < n + p.
-Proof. by move/leq_trans=> -> //; apply: leq_addr. Qed.
+Lemma leq_addr m n : n <= n + m. Proof. by rewrite addnC leq_addl. Qed.
 
 Lemma ltn_addl m n p : m < n -> m < p + n.
 Proof. by move/leq_trans=> -> //; apply: leq_addl. Qed.
 
+Lemma ltn_addr m n p : m < n -> m < n + p.
+Proof. by move/leq_trans=> -> //; apply: leq_addr. Qed.
+
 Lemma addn_gt0 m n : (0 < m + n) = (0 < m) || (0 < n).
 Proof. by rewrite !lt0n -negb_and addn_eq0. Qed.
 
@@ -536,7 +534,7 @@ Lemma subnK m n : m <= n -> (n - m) + m = n.
 Proof. by rewrite addnC; apply: subnKC. Qed.
 
 Lemma addnBA m n p : p <= n -> m + (n - p) = m + n - p.
-Proof. by move=> le_pn; rewrite -{2}(subnK le_pn) addnA addnK. Qed.
+Proof. by move=> le_pn; rewrite -[in RHS](subnK le_pn) addnA addnK. Qed.
 
 Lemma addnBAC m n p : n <= m -> m - n + p = m + p - n.
 Proof. by move=> le_nm; rewrite addnC addnBA // addnC. Qed.
@@ -548,7 +546,7 @@ Lemma addnABC m n p : p <= m -> p <= n -> m + (n - p) = m - p + n.
 Proof. by move=> le_pm le_pn; rewrite addnBA // addnBAC. Qed.
 
 Lemma subnBA m n p : p <= n -> m - (n - p) = m + p - n.
-Proof. by move=> le_pn; rewrite -{2}(subnK le_pn) subnDr. Qed.
+Proof. by move=> le_pn; rewrite -[in RHS](subnK le_pn) subnDr. Qed.
 
 Lemma subKn m n : m <= n -> n - (n - m) = m.
 Proof. by move/subnBA->; rewrite addKn. Qed.
@@ -556,16 +554,13 @@ Proof. by move/subnBA->; rewrite addKn. Qed.
 Lemma subSn m n : m <= n -> n.+1 - m = (n - m).+1.
 Proof. by rewrite -add1n => /addnBA <-. Qed.
 
-Lemma subnSK m n : m < n -> (n - m.+1).+1 = n - m.
-Proof. by move/subSn. Qed.
+Lemma subnSK m n : m < n -> (n - m.+1).+1 = n - m. Proof. by move/subSn. Qed.
 
 Lemma predn_sub m n : (m - n).-1 = (m.-1 - n).
 Proof. by case: m => // m; rewrite subSKn. Qed.
 
 Lemma leq_sub2r p m n : m <= n -> m - p <= n - p.
-Proof.
-by move=> le_mn; rewrite leq_subLR (leq_trans le_mn) // -leq_subLR.
-Qed.
+Proof. by move=> le_mn; rewrite leq_subLR (leq_trans le_mn) // -leq_subLR. Qed.
 
 Lemma leq_sub2l p m n : m <= n -> p - n <= p - m.
 Proof.
@@ -719,7 +714,7 @@ Proof. by move=> n; apply/minn_idPl. Qed.
 Lemma leq_min m n1 n2 : (m <= minn n1 n2) = (m <= n1) && (m <= n2).
 Proof.
 wlog le_n21: n1 n2 / n2 <= n1.
-  by case/orP: (leq_total n2 n1) => ?; last rewrite minnC andbC; auto.
+  by case/orP: (leq_total n2 n1) => ?; last rewrite minnC andbC; apply.
 rewrite /minn ltnNge le_n21 /=; case le_m_n1: (m <= n1) => //=.
 apply/contraFF: le_m_n1 => /leq_trans; exact.
 Qed.
@@ -1032,7 +1027,7 @@ Lemma leq_pmulr m n : n > 0 -> m <= m * n.
 Proof. by move/leq_pmull; rewrite mulnC. Qed.
 
 Lemma leq_mul2l m n1 n2 : (m * n1 <= m * n2) = (m == 0) || (n1 <= n2).
-Proof. by rewrite {1}/leq -mulnBr muln_eq0. Qed.
+Proof. by rewrite [LHS]/leq -mulnBr muln_eq0. Qed.
 
 Lemma leq_mul2r m n1 n2 : (n1 * m <= n2 * m) = (m == 0) || (n1 <= n2).
 Proof. by rewrite -!(mulnC m) leq_mul2l. Qed.
@@ -1081,7 +1076,7 @@ Proof. by move/prednK <-; rewrite ltn_mul2r. Qed.
 Arguments ltn_pmul2r [m n1 n2].
 
 Lemma ltn_Pmull m n : 1 < n -> 0 < m -> m < n * m.
-Proof. by move=> lt1n m_gt0; rewrite -{1}[m]mul1n ltn_pmul2r. Qed.
+Proof. by move=> lt1n m_gt0; rewrite -[m in m < _]mul1n ltn_pmul2r. Qed.
 
 Lemma ltn_Pmulr m n : 1 < n -> 0 < m -> m < m * n.
 Proof. by move=> lt1n m_gt0; rewrite mulnC ltn_Pmull. Qed.
@@ -1286,7 +1281,7 @@ Lemma muln2 m : m * 2 = m.*2.
 Proof. by rewrite mulnC mul2n. Qed.
 
 Lemma doubleD m n : (m + n).*2 = m.*2 + n.*2.
-Proof. by rewrite -!addnn -!addnA (addnCA n). Qed.
+Proof. by rewrite -!mul2n mulnDr. Qed.
 
 Lemma doubleB m n : (m - n).*2 = m.*2 - n.*2.
 Proof. by elim: m n => [|m IHm] []. Qed.
@@ -1346,7 +1341,8 @@ Proof. by case: b; rewrite /= (half_double, uphalf_double). Qed.
 
 Lemma halfD m n : (m + n)./2 = (odd m && odd n) + (m./2 + n./2).
 Proof.
-rewrite -{1}[n]odd_double_half addnCA -{1}[m]odd_double_half -addnA -doubleD.
+rewrite -[n in LHS]odd_double_half addnCA.
+rewrite -[m in LHS]odd_double_half -addnA -doubleD.
 by do 2!case: odd; rewrite /= ?add0n ?half_double ?uphalf_double.
 Qed.
 
@@ -1358,7 +1354,7 @@ Proof. by case: n => [|[]]. Qed.
 
 Lemma odd_geq m n : odd n -> (m <= n) = (m./2.*2 <= n).
 Proof.
-move=> odd_n; rewrite -{1}[m]odd_double_half -[n]odd_double_half odd_n.
+move=> odd_n; rewrite -[m in LHS]odd_double_half -[n]odd_double_half odd_n.
 by case: (odd m); rewrite // leq_Sdouble ltnS leq_double.
 Qed.
 
@@ -1383,8 +1379,8 @@ Qed.
 
 Lemma sqrn_sub m n : n <= m -> (m - n) ^ 2 = m ^ 2 + n ^ 2 - 2 * (m * n).
 Proof.
-move/subnK=> def_m; rewrite -{2}def_m sqrnD -addnA addnAC.
-by rewrite -2!addnA addnn -mul2n -mulnDr -mulnDl def_m addnK.
+move/subnK <-; rewrite addnK sqrnD -addnA -addnACA -addnA.
+by rewrite addnn -mul2n -mulnDr -mulnDl addnK.
 Qed.
 
 Lemma sqrnD_sub m n : n <= m -> (m + n) ^ 2 - 4 * (m * n) = (m - n) ^ 2.
@@ -1394,7 +1390,7 @@ by rewrite sqrnD addnK sqrn_sub.
 Qed.
 
 Lemma subn_sqr m n : m ^ 2 - n ^ 2 = (m - n) * (m + n).
-Proof. by rewrite mulnBl !mulnDr addnC (mulnC m) subnDl !mulnn. Qed.
+Proof. by rewrite mulnBl !mulnDr addnC (mulnC m) subnDl. Qed.
 
 Lemma ltn_sqr m n : (m ^ 2 < n ^ 2) = (m < n).
 Proof. by rewrite ltn_exp2r. Qed.
@@ -1440,8 +1436,7 @@ Lemma leqif_trans m1 m2 m3 C12 C23 :
   m1 <= m2 ?= iff C12 -> m2 <= m3 ?= iff C23 -> m1 <= m3 ?= iff C12 && C23.
 Proof.
 move=> ltm12 ltm23; apply/leqifP; rewrite -ltm12.
-case eqm12: (m1 == m2).
-  by rewrite (eqP eqm12) ltn_neqAle !ltm23 andbT; case C23.
+have [->|eqm12] := eqVneq; first by rewrite ltn_neqAle !ltm23 andbT; case C23.
 by rewrite (@leq_trans m2) ?ltm23 // ltn_neqAle eqm12 ltm12.
 Qed.
 
@@ -1491,15 +1486,15 @@ Qed.
 Lemma nat_Cauchy m n : 2 * (m * n) <= m ^ 2 + n ^ 2 ?= iff (m == n).
 Proof.
 without loss le_nm: m n / n <= m.
-  by case: (leqP m n); auto; rewrite eq_sym addnC (mulnC m); auto.
-apply/leqifP; case: ifP => [/eqP-> | ne_mn]; first by rewrite mulnn addnn mul2n.
+  by have [?|/ltnW ?] := leqP n m; last rewrite eq_sym addnC (mulnC m); apply.
+apply/leqifP; have [-> | ne_mn] := eqVneq; first by rewrite addnn mul2n.
 by rewrite -subn_gt0 -sqrn_sub // sqrn_gt0 subn_gt0 ltn_neqAle eq_sym ne_mn.
 Qed.
 
 Lemma nat_AGM2 m n : 4 * (m * n) <= (m + n) ^ 2 ?= iff (m == n).
 Proof.
 rewrite -[4]/(2 * 2) -mulnA mul2n -addnn sqrnD; apply/leqifP.
-by rewrite ltn_add2r eqn_add2r ltn_neqAle !nat_Cauchy; case: ifP => ->.
+by rewrite ltn_add2r eqn_add2r ltn_neqAle !nat_Cauchy; case: eqVneq.
 Qed.
 
 Section Monotonicity.
@@ -1530,7 +1525,7 @@ Lemma homo_leq_in (D : {pred nat}) (f : nat -> T) (r : T -> T -> Prop) :
   {in D &, {homo f : i j / i <= j >-> r i j}}.
 Proof.
 move=> r_refl r_trans Dcx /(homo_ltn_in r_trans Dcx) lt_r i j iD jD.
-by rewrite leq_eqVlt => /predU1P[->//|/lt_r]; apply.
+case: ltngtP => [? _||->] //; exact: lt_r.
 Qed.
 
 Lemma homo_leq (f : nat -> T) (r : T -> T -> Prop) :
@@ -1694,7 +1689,7 @@ Proof. by move=> m [|n] //=; rewrite mul_expE expnS mulnC. Qed.
 
 Lemma oddE : odd =1 oddn.
 Proof.
-move=> n; rewrite -{1}[n]odd_double_half addnC.
+move=> n; rewrite -[n in LHS]odd_double_half addnC.
 by elim: n./2 => //=; case (oddn n).
 Qed.
 
@@ -1707,7 +1702,7 @@ Notation natTrecE := NatTrec.trecE.
 Lemma eq_binP : Equality.axiom N.eqb.
 Proof.
 move=> p q; apply: (iffP idP) => [|<-]; last by case: p => //; elim.
-by case: q; case: p => //; elim=> [p IHp|p IHp|] [q|q|] //=; case/IHp=> ->.
+by case: q; case: p => //; elim=> [p IHp|p IHp|] [q|q|] //= /IHp [->].
 Qed.
 
 Canonical bin_nat_eqMixin := EqMixin eq_binP.
@@ -1816,9 +1811,7 @@ Proof. exact: mk_srt add0n addnC addnA mul1n mul0n mulnC mulnA mulnDl. Qed.
 
 Lemma nat_semi_morph :
   semi_morph 0 1 addn muln (@eq _) 0%num 1%num Nplus Nmult pred1 nat_of_bin.
-Proof.
-by move: nat_of_add_bin nat_of_mul_bin; split=> //= m n; move/eqP->.
-Qed.
+Proof. by move: nat_of_add_bin nat_of_mul_bin; split=> //= m n /eqP ->. Qed.
 
 Lemma nat_power_theory : power_theory 1 muln (@eq _) nat_of_bin expn.
 Proof. by split; apply: nat_of_exp_bin. Qed.
diff --git a/mathcomp/ssreflect/tuple.v b/mathcomp/ssreflect/tuple.v
index 551dc779b8..db53235619 100644
--- a/mathcomp/ssreflect/tuple.v
+++ b/mathcomp/ssreflect/tuple.v
@@ -351,8 +351,8 @@ rewrite count_filter -(@eq_count _ (pred1 t)) => [|s /=]; last first.
   by rewrite isSome_insub; case: eqP=> // ->.
 elim: n t t_n => [|m IHm] [|x t] //= {IHm}/IHm; move: (iter m _ _) => em IHm.
 transitivity (x \in T : nat); rewrite // -mem_enum codomE.
-elim: (fintype.enum T)  (enum_uniq T) => //= y e IHe /andP[/negPf ney].
-rewrite count_cat count_map inE /preim /= {1}/eq_op /= eq_sym => /IHe->.
+elim: (fintype.enum T) (enum_uniq T) => //= y e IHe /andP[/negPf ney].
+rewrite count_cat count_map inE /preim /= [in LHS]/eq_op /= eq_sym => /IHe->.
 by case: eqP => [->|_]; rewrite ?(ney, count_pred0, IHm).
 Qed.