From 43129d5077d68b2ae67c2480bc1ed9b760071012 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 5 Apr 2022 18:18:37 +0900
Subject: [PATCH 1/3] pattern for rewriting Boolean (in)equalities

---
 mathcomp/algebra/rat.v       |  4 ++--
 mathcomp/character/inertia.v | 14 +++++++-------
 mathcomp/ssreflect/eqtype.v  |  5 +++++
 mathcomp/ssreflect/order.v   | 11 +++++++++++
 mathcomp/ssreflect/prime.v   |  8 ++++----
 5 files changed, 29 insertions(+), 13 deletions(-)

diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 1b9155a926..19353adaba 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -306,7 +306,7 @@ Lemma rat_eq x y : (x == y) = (numq x * denq y == numq y * denq x).
 Proof.
 symmetry; rewrite rat_eqE andbC.
 have [->|] /= := eqVneq (denq _); first by rewrite (inj_eq (mulIf _)).
-apply: contraNF => /eqP hxy; rewrite -absz_denq -[X in _ == X]absz_denq.
+apply: contraNF => /eqP hxy; rewrite -absz_denq -[eqRHS]absz_denq.
 rewrite eqz_nat /= eqn_dvd.
 rewrite -(@Gauss_dvdr _ `|numq x|) 1?coprime_sym ?coprime_num_den // andbC.
 rewrite -(@Gauss_dvdr _ `|numq y|) 1?coprime_sym ?coprime_num_den //.
@@ -317,7 +317,7 @@ Fact fracq_eq x y : x.2 != 0 -> y.2 != 0 ->
   (fracq x == fracq y) = (x.1 * y.2 == y.1 * x.2).
 Proof.
 case: fracqP=> //= u fx u_neq0 _; case: fracqP=> //= v fy v_neq0 _; symmetry.
-rewrite [X in (_ == X)]mulrC mulrACA [X in (_ == X)]mulrACA.
+rewrite [eqRHS]mulrC mulrACA [eqRHS]mulrACA.
 by rewrite [denq _ * _]mulrC (inj_eq (mulfI _)) ?mulf_neq0 // rat_eq.
 Qed.
 
diff --git a/mathcomp/character/inertia.v b/mathcomp/character/inertia.v
index 6ab16d7b75..371b5523f7 100644
--- a/mathcomp/character/inertia.v
+++ b/mathcomp/character/inertia.v
@@ -170,7 +170,7 @@ Section Inertia.
 
 Variable gT : finGroupType.
 
-Definition inertia (B : {set gT}) (phi : 'CF(B)) :=  
+Definition inertia (B : {set gT}) (phi : 'CF(B)) :=
   [set y in 'N(B) | (phi ^ y)%CF == phi].
 
 Local Notation "''I[' phi ]" := (inertia phi) : group_scope.
@@ -380,7 +380,7 @@ move=> nsHG Gy; rewrite -conjg_IirrE cfdot_irr -(inj_eq irr_inj) conjg_IirrE.
 by rewrite -{1}['chi_i]cfConjgJ1 cfConjg_eqE ?mulg1.
 Qed.
 
-Definition cfclass (A : {set gT}) (phi : 'CF(A)) (B : {set gT}) := 
+Definition cfclass (A : {set gT}) (phi : 'CF(A)) (B : {set gT}) :=
   [seq (phi ^ repr Tx)%CF | Tx in rcosets 'I_B[phi] B].
 
 Local Notation "phi ^: G" := (cfclass phi G) : cfun_scope.
@@ -498,7 +498,7 @@ Qed.
 (* This is Isaacs, Theorem (6.2) *)
 Lemma Clifford_Res_sum_cfclass i j :
      H <| G -> j \in irr_constt ('Res[H, G] 'chi_i) ->
-  'Res[H] 'chi_i = 
+  'Res[H] 'chi_i =
      '['Res[H] 'chi_i, 'chi_j] *: (\sum_(chi <- ('chi_j ^: G)%CF) chi).
 Proof.
 move=> nsHG chiHj; have [sHG /subsetP nHG] := andP nsHG.
@@ -1063,7 +1063,7 @@ rewrite gt_eqF // (bigD1 b) //= cfdotZl cfnorm_irr mulr1 ltr_paddr ?egt0 //.
 apply: sumr_ge0 => g /andP[Sg _]; rewrite cfdotZl cfdot_irr.
 by rewrite mulr_ge0 ?ler0n ?Cnat_ge0.
 Qed.
-  
+
 (* This is Isaacs, Corollary (6.17) (due to Gallagher). *)
 Corollary constt_Ind_ext :
   [/\ forall b : Iirr (G / N), 'chi_(mod_Iirr b) * chi \in irr G,
@@ -1175,7 +1175,7 @@ have [inj_Mphi | /injectivePn[i [j i'j eq_mm_ij]]] := boolP (injectiveb mmLth).
   rewrite ler_paddr ?sumr_ge0 // => [i _|].
     by rewrite char1_ge0 ?rpredZ_Cnat ?Cnat_cfdot_char ?cfInd_char ?irr_char.
   rewrite -big_uniq //= big_image -sumr_const ler_sum // => i _.
-  rewrite cfunE -[in rhs in _ <= rhs](cfRes1 L) -cfdot_Res_r mmLthL cfRes1.
+  rewrite cfunE -[in leRHS](cfRes1 L) -cfdot_Res_r mmLthL cfRes1.
   by rewrite DthL cfdotZr rmorph_nat cfnorm_irr mulr1.
 constructor 2; exists e; first by exists p0.
 pose mu := (('chi_i / 'chi_j)%R %% L)%CF; pose U := cfker mu.
@@ -1299,7 +1299,7 @@ have{} Dc2: 'chi_c2 = ('chi_s2 %% N)%CF * 'chi_c.
   by rewrite Dc2 cfIirrE // mod_IirrE.
 have s2_lin: 'chi_s2 \is a linear_char.
   rewrite qualifE irr_char; apply/eqP/(mulIf (irr1_neq0 c)).
-  rewrite mul1r -[in rhs in _ = rhs](cfRes1 N) chiN -c2Nth cfRes1.
+  rewrite mul1r -[in RHS](cfRes1 N) chiN -c2Nth cfRes1.
   by rewrite Dc2 cfunE cfMod1.
 have s2Xf_1: 'chi_s2 ^+ f = 1.
   apply/(can_inj (cfModK nsNG))/(mulIr (lin_char_unitr lin_mu))/esym.
@@ -1313,7 +1313,7 @@ Qed.
 (* This is Isaacs, Theorem (6.25). *)
 Theorem solvable_irr_extendible_from_det G N s (theta := 'chi[N]_s) :
     N <| G -> solvable (G / N) ->
-    G \subset 'I[theta] -> coprime #|G : N| (truncC (theta 1%g)) -> 
+    G \subset 'I[theta] -> coprime #|G : N| (truncC (theta 1%g)) ->
   [exists c, 'Res 'chi[G]_c == theta]
     = [exists u, 'Res 'chi[G]_u == cfDet theta].
 Proof.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index eb95b360de..39b9a8e6be 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -38,6 +38,8 @@ From mathcomp Require Import ssreflect ssrfun ssrbool.
 (*         x != y :> T <=> x and y compare unequal at type T.                 *)
 (*             x =P y  :: a proof of reflect (x = y) (x == y); x =P y coerces *)
 (*                     to x == y -> x = y.                                    *)
+(*               eqLHS := (X in (X == _))%pattern (for rewriting)             *)
+(*               eqRHS := (X in (_ == X))%pattern (for rewriting)             *)
 (*               eq_op == the boolean relation behind the == notation.        *)
 (*             pred1 a == the singleton predicate [pred x | x == a].          *)
 (* pred2, pred3, pred4 == pair, triple, quad predicates.                      *)
@@ -189,6 +191,9 @@ Notation "x =P y" := (eqP : reflect (x = y) (x == y))
 Notation "x =P y :> T" := (eqP : reflect (x = y :> T) (x == y :> T))
   (at level 70, y at next level, no associativity) : eq_scope.
 
+Notation eqLHS := (X in (X == _))%pattern.
+Notation eqRHS := (X in (_ == X))%pattern.
+
 Prenex Implicits eq_op eqP.
 
 Lemma eq_refl (T : eqType) (x : T) : x == x. Proof. exact/eqP. Qed.
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 2404bef033..3829757cdb 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -215,6 +215,12 @@ From mathcomp Require Import finset.
 (* with head symbols Order.arg_min and Order.arg_max                          *)
 (* The user may use extremumP or extremum_inP to eliminate them.              *)
 (*                                                                            *)
+(* -> patterns for contextual rewriting:                                      *)
+(*      leLHS := (X in (X <= _)%O)%pattern                                    *)
+(*      leRHS := (X in (_ <= X)%O)%pattern                                    *)
+(*      ltLHS := (X in (X < _)%O)%pattern                                     *)
+(*      ltRHS := (X in (_ < X)%O)%pattern                                     *)
+(*                                                                            *)
 (* In order to build the above structures, one must provide the appropriate   *)
 (* factory instance to the following structure constructors. The list of      *)
 (* possible factories is indicated after each constructor. Each factory is    *)
@@ -1240,6 +1246,11 @@ Notation "[ 'arg' 'max_' ( i > i0 ) F ]" := [arg max_(i > i0 | true) F]
   (at level 0, i, i0 at level 10,
    format "[ 'arg'  'max_' ( i  >  i0 ) F ]") : order_scope.
 
+Notation leLHS := (X in (X <= _)%O)%pattern.
+Notation leRHS := (X in (_ <= X)%O)%pattern.
+Notation ltLHS := (X in (X < _)%O)%pattern.
+Notation ltRHS := (X in (_ < X)%O)%pattern.
+
 End POSyntax.
 
 Module POCoercions.
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index c60b72a902..4c47eaa9de 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -969,9 +969,9 @@ Lemma up_lognn p : 1 < p -> up_log p p = 1.
 Proof. by move=> p_gt1; apply: up_log_eq; rewrite p_gt1 /=. Qed.
 
 Lemma up_expnK p n : 1 < p -> up_log p (p ^ n) = n.
-Proof. 
+Proof.
 case: n => [|n] p_gt1 /=; first by rewrite up_log1.
-by apply: up_log_eq; rewrite // leqnn andbT ltn_exp2l. 
+by apply: up_log_eq; rewrite // leqnn andbT ltn_exp2l.
 Qed.
 
 Lemma up_logMp p n : 1 < p -> 0 < n -> up_log p (p * n) = (up_log p n).+1.
@@ -1003,7 +1003,7 @@ rewrite mul2n !doubleS !ltnS.
 by rewrite -[X in X <= _]odd_double_half -add1n leq_add2r; case: odd.
 Qed.
 
-Lemma up_log_trunc_log p n : 
+Lemma up_log_trunc_log p n :
   1 < p -> 1 < n -> up_log p n = (trunc_log p n.-1).+1.
 Proof.
 move=> p_gt1 n_gt1; apply: up_log_eq => //.
@@ -1011,7 +1011,7 @@ rewrite -[n]prednK ?ltnS -?pred_Sn ?[0 < n]ltnW//.
 by rewrite trunc_logP ?ltn_predRL// trunc_log_ltn.
 Qed.
 
-Lemma trunc_log_up_log p n : 
+Lemma trunc_log_up_log p n :
   1 < p -> 0 < n -> trunc_log p n = (up_log p n.+1).-1.
 Proof. by move=> ? ?; rewrite up_log_trunc_log.
 Qed.

From 9a3a1a797c80b393f37b1985071f20dc38c75692 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 5 Apr 2022 18:25:20 +0900
Subject: [PATCH 2/3] update changelog

---
 CHANGELOG_UNRELEASED.md        |  8 +++++
 mathcomp/algebra/fraction.v    |  4 +--
 mathcomp/algebra/mxpoly.v      |  6 ++--
 mathcomp/algebra/poly.v        |  2 +-
 mathcomp/algebra/polyXY.v      |  2 +-
 mathcomp/algebra/polydiv.v     |  4 +--
 mathcomp/algebra/rat.v         |  4 +--
 mathcomp/character/character.v | 66 +++++++++++++++++-----------------
 mathcomp/solvable/abelian.v    |  2 +-
 mathcomp/ssreflect/div.v       |  8 ++---
 mathcomp/ssreflect/eqtype.v    |  8 ++---
 mathcomp/ssreflect/order.v     |  6 ++--
 mathcomp/ssreflect/prime.v     | 30 ++++++++--------
 mathcomp/ssreflect/ssrnat.v    | 13 ++++++-
 14 files changed, 91 insertions(+), 72 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index ba9ae62f36..3885fc5e3c 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -37,6 +37,14 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/).
 - in `ssrbool.v`, added lemma `all_sig2_cond`
 - in `choice.v`, added coercion `Choice.mixin`
 - In `seq.v`, added lemmas `mkseqS`, `mkseq_uniqP`
+- in `eqtype.v`:
+  + notations `eqbLHS` and `eqbRHS`
+
+- in `order.v`:
+  + notations `leLHS`, `leRHS`, `ltLHS`, `ltRHS`
+
+- in `ssrnat.v`:
+  + notations `leqLHS`, `leqRHS`, `ltnLHS`, `ltnRHS`
 
 ### Changed
 
diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v
index 1da8f137bf..10564b930e 100644
--- a/mathcomp/algebra/fraction.v
+++ b/mathcomp/algebra/fraction.v
@@ -341,7 +341,7 @@ Local Notation "x %:F" := (tofrac x).
 Lemma tofrac_is_additive: additive tofrac.
 Proof.
 move=> p q /=; unlock tofrac.
-rewrite -[X in _ = _ + X]pi_opp -[X in _ = X]pi_add.
+rewrite -[X in _ = _ + X]pi_opp -[RHS]pi_add.
 by rewrite /addf /oppf /= !numden_Ratio ?(oner_neq0, mul1r, mulr1).
 Qed.
 
@@ -349,7 +349,7 @@ Canonical tofrac_additive := Additive tofrac_is_additive.
 
 Lemma tofrac_is_multiplicative: multiplicative tofrac.
 Proof.
-split=> [p q|//]; unlock tofrac; rewrite -[X in _ = X]pi_mul.
+split=> [p q|//]; unlock tofrac; rewrite -[RHS]pi_mul.
 by rewrite /mulf /= !numden_Ratio ?(oner_neq0, mul1r, mulr1).
 Qed.
 
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index 544b734eba..000a612d23 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -218,7 +218,7 @@ pose S_ j1 := map_mx polyC (\matrix_(i, j) S i (if j == j0 then j1 else j)).
 pose Ss0_ i dj := \poly_(j < dj) S i (insubd j0 j).
 pose Ss_ dj := \matrix_(i, j) (if j == j0 then Ss0_ i dj else (S i j)%:P).
 have{Ss u} ->: Ss = Ss_ dS.
-  apply/matrixP=> i j; rewrite mxE [in X in _ = X]mxE; case: (j == j0) => {j}//.
+  apply/matrixP=> i j; rewrite mxE [in RHS]mxE; case: (j == j0) => {j}//.
   apply/polyP=> k; rewrite coef_poly Sylvester_mxE mxE.
   have [k_ge_dS | k_lt_dS] := leqP dS k.
     case: (split i) => {}i; rewrite !mxE coefMXn;
@@ -242,7 +242,7 @@ rewrite -det_tr => /determinant_multilinear->;
 have [dj0 | dj_gt0] := posnP dj; rewrite ?dj0 !mul1r.
   rewrite !det_tr det_map_mx addrC (expand_det_col _ j0) big1 => [|i _].
     rewrite add0r; congr (\det _)%:P.
-    apply/matrixP=> i j; rewrite [in X in _ = X]mxE; case: eqP => // ->.
+    apply/matrixP=> i j; rewrite [in RHS]mxE; case: eqP => // ->.
     by congr (S i _); apply: val_inj.
   by rewrite mxE /= [Ss0_ _ _]poly_def big_ord0 mul0r.
 have /determinant_alternate->: j1 != j0 by rewrite -val_eqE -lt0n.
@@ -1783,7 +1783,7 @@ apply/diagonalizable_forPex/'forall_diagonalizable_forPex => /=
   by exists D0; apply/simmxW.
 exists (\mxrow_i tag (DoA i)); apply/simmxW.
    rewrite -row_leq_rank eqmx_col (mxdirectP Vd)/=.
-   by under [X in (_ <= X)%N]eq_bigr do rewrite genmxE (eqP (rAV _)).
+   by under [leqRHS]eq_bigr do rewrite genmxE (eqP (rAV _)).
 rewrite mxcol_mul diag_mxrow mul_mxdiag_mxcol; apply: eq_mxcol => i.
 by case: DoA => /= k /(simmxPp); rewrite VA => /(_ isT) ->.
 Qed.
diff --git a/mathcomp/algebra/poly.v b/mathcomp/algebra/poly.v
index 61bc5ad025..cfe5c956b7 100644
--- a/mathcomp/algebra/poly.v
+++ b/mathcomp/algebra/poly.v
@@ -2381,7 +2381,7 @@ have [/size1_polyC-> | nc_q] := leqP (size q) 1.
 have nz_q: q != 0 by rewrite -size_poly_eq0 -(subnKC nc_q).
 rewrite mulnC comp_polyE (polySpred nz_p) /= big_ord_recr /= addrC.
 rewrite size_addl size_scale ?lead_coef_eq0 ?size_exp //=.
-rewrite [X in _ < X]polySpred ?expf_neq0 // ltnS size_exp.
+rewrite [ltnRHS]polySpred ?expf_neq0 // ltnS size_exp.
 rewrite (leq_trans (size_sum _ _ _)) //; apply/bigmax_leqP => i _.
 rewrite (leq_trans (size_scale_leq _ _)) // polySpred ?expf_neq0 //.
 by rewrite size_exp -(subnKC nc_q) ltn_pmul2l.
diff --git a/mathcomp/algebra/polyXY.v b/mathcomp/algebra/polyXY.v
index fe0acb488a..63a0c76d84 100644
--- a/mathcomp/algebra/polyXY.v
+++ b/mathcomp/algebra/polyXY.v
@@ -268,7 +268,7 @@ rewrite ltn_eqF // !rmorphM !lead_coefM (leq_trans (leq_ltn_trans _ ltuq)) //=.
   by rewrite mulrC mul_polyC size_scale ?max_size_lead_coefXY ?lead_coef_eq0.
 rewrite swapXY_map_polyC lead_coefC size_map_polyC.
 set v1 := lead_coef _; have nz_v1: v1 != 0 by rewrite lead_coef_eq0 swapXY_eq0.
-rewrite [in rhs in _ <= rhs]polySpred ?mulf_neq0 // size_mul //.
+rewrite [leqRHS]polySpred ?mulf_neq0 // size_mul //.
 by rewrite (polySpred nz_v1) addnC addnS polySpred // ltnS leq_addr.
 Qed.
 
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index 266bdbc9c6..8e8592c776 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -170,7 +170,7 @@ apply: ihn => //.
 - apply/leq_sizeP => j hnj.
   rewrite coefB -scalerAl coefZ coefXnM ltn_subRL ltnNge.
   have hj : (size r).-1 <= j by apply: leq_trans hnj; rewrite -ltnS prednK.
-  rewrite [r in r <= _]polySpred -?size_poly_gt0 // coefMC.
+  rewrite [leqLHS]polySpred -?size_poly_gt0 // coefMC.
   rewrite (leq_ltn_trans hj) /=; last by rewrite -add1n leq_add2r.
   move: hj; rewrite leq_eqVlt prednK // => /predU1P [<- | hj].
     by rewrite -subn1 subnAC subKn // !subn1 !lead_coefE subrr.
@@ -1669,7 +1669,7 @@ Proof.
 have [-> | nn0] := eqVneq n 0; first by rewrite gcd0p mulr0 eqpxx.
 have [-> | mn0] := eqVneq m 0; first by rewrite mul0r gcdp0 eqpxx.
 rewrite gcdpE modp_mull gcd0p size_mul //; case: leqP; last by rewrite eqpxx.
-rewrite (polySpred mn0) addSn /= -[n in _ <= n]add0n leq_add2r -ltnS.
+rewrite (polySpred mn0) addSn /= -[leqRHS]add0n leq_add2r -ltnS.
 rewrite -polySpred //= leq_eqVlt ltnS size_poly_leq0 (negPf mn0) orbF.
 case/size_poly1P=> c cn0 -> {mn0 m}; rewrite mul_polyC.
 suff -> : n %% (c *: n) = 0 by rewrite gcd0p; apply: eqp_scale.
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 19353adaba..4cd6de442f 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -306,7 +306,7 @@ Lemma rat_eq x y : (x == y) = (numq x * denq y == numq y * denq x).
 Proof.
 symmetry; rewrite rat_eqE andbC.
 have [->|] /= := eqVneq (denq _); first by rewrite (inj_eq (mulIf _)).
-apply: contraNF => /eqP hxy; rewrite -absz_denq -[eqRHS]absz_denq.
+apply: contraNF => /eqP hxy; rewrite -absz_denq -[eqbRHS]absz_denq.
 rewrite eqz_nat /= eqn_dvd.
 rewrite -(@Gauss_dvdr _ `|numq x|) 1?coprime_sym ?coprime_num_den // andbC.
 rewrite -(@Gauss_dvdr _ `|numq y|) 1?coprime_sym ?coprime_num_den //.
@@ -317,7 +317,7 @@ Fact fracq_eq x y : x.2 != 0 -> y.2 != 0 ->
   (fracq x == fracq y) = (x.1 * y.2 == y.1 * x.2).
 Proof.
 case: fracqP=> //= u fx u_neq0 _; case: fracqP=> //= v fy v_neq0 _; symmetry.
-rewrite [eqRHS]mulrC mulrACA [eqRHS]mulrACA.
+rewrite [eqbRHS]mulrC mulrACA [eqbRHS]mulrACA.
 by rewrite [denq _ * _]mulrC (inj_eq (mulfI _)) ?mulf_neq0 // rat_eq.
 Qed.
 
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index 9dc1ecaf55..e646b4f004 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -85,9 +85,9 @@ Section Tensor.
 
 Variable (F : fieldType).
 
-Fixpoint trow  (n1 : nat) : 
+Fixpoint trow  (n1 : nat) :
   forall (A : 'rV[F]_n1) m2 n2 (B : 'M[F]_(m2,n2)), 'M[F]_(m2,n1 * n2) :=
-  if n1 is n'1.+1 
+  if n1 is n'1.+1
   then
     fun (A : 'M[F]_(1,(1 + n'1))) m2 n2 (B : 'M[F]_(m2,n2)) =>
        (row_mx (lsubmx A 0 0 *: B) (trow (rsubmx A) B))
@@ -117,9 +117,9 @@ case: split=> a.
 by rewrite linearD /= linearZ IH !mxE.
 Qed.
 
-Canonical Structure trowb_linear n1 m2 n2 B := 
+Canonical Structure trowb_linear n1 m2 n2 B :=
   Linear (@trowb_is_linear n1 m2 n2 B).
-  
+
 Lemma trow_is_linear n1 m2 n2 (A : 'rV_n1) : linear (@trow n1 A m2 n2).
 Proof.
 elim: n1 A => [|n1 IH] //= A k A1 A2 /=; first by rewrite scaler0 add0r.
@@ -128,13 +128,13 @@ apply/matrixP=> i j; rewrite !mxE.
 by case: split=> a; rewrite ?IH !mxE.
 Qed.
 
-Canonical Structure trow_linear n1 m2 n2 A := 
+Canonical Structure trow_linear n1 m2 n2 A :=
   Linear (@trow_is_linear n1 m2 n2 A).
 
-Fixpoint tprod  (m1 : nat) : 
+Fixpoint tprod  (m1 : nat) :
   forall n1 (A : 'M[F]_(m1,n1)) m2 n2 (B : 'M[F]_(m2,n2)),
         'M[F]_(m1 * m2,n1 * n2) :=
-  if m1 is m'1.+1 
+  if m1 is m'1.+1
     return forall n1 (A : 'M[F]_(m1,n1)) m2 n2 (B : 'M[F]_(m2,n2)),
            'M[F]_(m1 * m2,n1 * n2)
   then
@@ -155,8 +155,8 @@ Proof.
 by apply/matrixP=> i j /[!mxE]; apply: eq_bigr=> k _ /[!mxE].
 Qed.
 
-Let trow_mul (m1 m2 n2 p2 : nat) 
-         (A : 'rV_m1) (B1: 'M[F]_(m2,n2)) (B2 :'M[F]_(n2,p2)) : 
+Let trow_mul (m1 m2 n2 p2 : nat)
+         (A : 'rV_m1) (B1: 'M[F]_(m2,n2)) (B2 :'M[F]_(n2,p2)) :
   trow A (B1 *m B2) = B1 *m trow A B2.
 Proof.
 elim: m1 A => [|m1 IH] A /=; first by rewrite mulmx0.
@@ -255,7 +255,7 @@ Proof. by split=> // g h Hg Hx; rewrite mulmx1. Qed.
 
 Definition grepr0 := Representation (MxRepresentation mx_repr0).
 
-Lemma add_mx_repr (rG1 rG2 : representation) : 
+Lemma add_mx_repr (rG1 rG2 : representation) :
   mx_repr G (fun g => block_mx (rG1 g) 0 0 (rG2 g)).
 Proof.
 split=> [|x y Hx Hy]; first by rewrite !repr_mx1 -scalar_mx_block.
@@ -311,8 +311,8 @@ by rewrite -mulmxA (mulmxA _ fV).
 Qed.
 
 Lemma mx_rsim_dsum (I : finType) (P : pred I) U rU (W : 'M_n)
-    (modU : forall i, mxmodule rG (U i)) (modW : mxmodule rG W) : 
-    let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS -> mxdirect S -> 
+    (modU : forall i, mxmodule rG (U i)) (modW : mxmodule rG W) :
+    let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS -> mxdirect S ->
     (forall i, mx_rsim (submod_repr (modU i)) (rU i : representation)) ->
   mx_rsim (submod_repr modW) (\big[dadd_grepr/grepr0]_(i | P i) rU i).
 Proof.
@@ -1270,7 +1270,7 @@ Proof. by case/mulmx1_unit: XX'_1. Qed.
 Let uX := character_table_unit.
 
 (* This is Isaacs, Theorem (2.18). *)
-Theorem second_orthogonality_relation x y : 
+Theorem second_orthogonality_relation x y :
     y \in G ->
   \sum_i 'chi[G]_i x * ('chi_i y)^* = #|'C_G[x]|%:R *+ (x \in y ^: G).
 Proof.
@@ -1302,7 +1302,7 @@ Qed.
 
 (* This is Isaacs, Theorem (6.32) (due to Brauer). *)
 Lemma card_afix_irr_classes (ito : action A (Iirr G)) (cto : action A _) a :
-    a \in A -> [acts A, on classes G | cto] -> 
+    a \in A -> [acts A, on classes G | cto] ->
     (forall i x y, x \in G -> y \in cto (x ^: G) a ->
       'chi_i x = 'chi_(ito i a) y) ->
   #|'Fix_ito[a]| = #|'Fix_(classes G | cto)[a]|.
@@ -1380,7 +1380,7 @@ Lemma Cnat_cfdot_char_irr i phi :
   phi \is a character -> '[phi, 'chi_i]_G \in Cnat.
 Proof. by move/forallP/(_ i); rewrite coord_cfdot. Qed.
 
-Lemma cfdot_char_r phi chi :  
+Lemma cfdot_char_r phi chi :
   chi \is a character -> '[phi, chi]_G = \sum_i '[phi, 'chi_i] * '[chi, 'chi_i].
 Proof.
 move=> Nchi; rewrite cfdot_sum_irr; apply: eq_bigr => i _; congr (_ * _).
@@ -1393,7 +1393,7 @@ Proof.
 move=> Nchi Nxi; rewrite cfdot_char_r ?rpred_sum // => i _.
 by rewrite rpredM ?Cnat_cfdot_char_irr.
 Qed.
- 
+
 Lemma cfdotC_char chi xi :
   chi \is a character-> xi \is a character -> '[chi, xi]_G = '[xi, chi].
 Proof. by move=> Nchi Nxi; rewrite cfdotC conj_Cnat ?Cnat_cfdot_char. Qed.
@@ -1544,14 +1544,14 @@ Proof.
 by move=> j; rewrite !inE cfdot_irr pnatr_eq0 (eq_sym j); case: (i == j).
 Qed.
 
-Lemma char1_ge_constt (i : Iirr G) chi : 
+Lemma char1_ge_constt (i : Iirr G) chi :
   chi \is a character -> i \in irr_constt chi -> 'chi_i 1%g <= chi 1%g.
 Proof.
 move=> {chi} _ /constt_charP[// | chi Nchi ->].
 by rewrite cfunE addrC -subr_ge0 addrK char1_ge0.
 Qed.
 
-Lemma constt_ortho_char (phi psi : 'CF(G)) i j : 
+Lemma constt_ortho_char (phi psi : 'CF(G)) i j :
      phi \is a character -> psi \is a character ->
      i \in irr_constt phi -> j \in irr_constt psi ->
   '[phi, psi] = 0 -> '['chi_i, 'chi_j] = 0.
@@ -1571,7 +1571,7 @@ Section Kernel.
 Variable (gT : finGroupType) (G : {group gT}).
 Implicit Types (phi chi xi : 'CF(G)) (H : {group gT}).
 
-Lemma cfker_repr n (rG : mx_representation algCF G n) : 
+Lemma cfker_repr n (rG : mx_representation algCF G n) :
   cfker (cfRepr rG) = rker rG.
 Proof.
 apply/esym/setP=> x; rewrite inE mul1mx /=.
@@ -1580,7 +1580,7 @@ apply/eqP/idP=> Kx; last by rewrite max_cfRepr_mx1 // cfker1.
 rewrite inE Gx; apply/forallP=> y; rewrite !cfunE !mulrb groupMl //.
 by case: ifP => // Gy; rewrite repr_mxM // Kx mul1mx.
 Qed.
-  
+
 Lemma cfkerEchar chi :
   chi \is a character -> cfker chi = [set x in G | chi x == chi 1%g].
 Proof.
@@ -1743,7 +1743,7 @@ Lemma constt_Ind_Res i j :
 Proof. by rewrite !irr_consttE cfdotC conjC_eq0 -cfdot_Res_l. Qed.
 
 Lemma cfdot_Res_ge_constt i j psi :
-    psi \is a character -> j \in irr_constt psi -> 
+    psi \is a character -> j \in irr_constt psi ->
   '['Res[H, G] 'chi_j, 'chi_i] <= '['Res[H] psi, 'chi_i].
 Proof.
 move=> {psi} _ /constt_charP[// | psi Npsi ->].
@@ -1752,7 +1752,7 @@ by rewrite Cnat_cfdot_char_irr // cfRes_char.
 Qed.
 
 Lemma constt_Res_trans j psi :
-    psi \is a character -> j \in irr_constt psi -> 
+    psi \is a character -> j \in irr_constt psi ->
   {subset irr_constt ('Res[H, G] 'chi_j) <= irr_constt ('Res[H] psi)}.
 Proof.
 move=> Npsi Cj i; apply: contraNneq; rewrite eq_le => {1}<-.
@@ -2204,7 +2204,7 @@ Qed.
 Lemma conjC_irrAut u i x : (u ('chi[G]_i x))^* = u ('chi_i x)^*.
 Proof. exact: conjC_charAut (irr_char i). Qed.
 
-Lemma cfdot_aut_char u (phi chi : 'CF(G)) : 
+Lemma cfdot_aut_char u (phi chi : 'CF(G)) :
   chi \is a character -> '[cfAut u phi, cfAut u chi] = u '[phi, chi].
 Proof. by move/conjC_charAut=> Nchi; apply: cfdot_cfAut => _ /mapP[x _ ->]. Qed.
 
@@ -2436,7 +2436,7 @@ apply: contraNneq ntx => i0; apply/eqP/inj_chi=> //.
 by rewrite i0 irr0 !cfun1E Gx group1.
 Qed.
 
-(* This is Isaacs (2.23)(a). *) 
+(* This is Isaacs (2.23)(a). *)
 Lemma cap_cfker_lin_irr G :
   \bigcap_(i | 'chi[G]_i \is a linear_char) (cfker 'chi_i) = G^`(1)%g.
 Proof.
@@ -2452,7 +2452,7 @@ have nsG'G := der_normal 1 G; rewrite (eq_card (@lin_irr_der1 G)).
 rewrite -(on_card_preimset (mod_Iirr_bij nsG'G)).
 rewrite -card_quotient ?normal_norm //.
 move: (der_abelian 0 G); rewrite card_classes_abelian; move/eqP<-.
-rewrite -NirrE -[X in _ = X]card_ord.
+rewrite -NirrE -[RHS]card_ord.
 by apply: eq_card => i; rewrite !inE mod_IirrE ?cfker_mod.
 (* Alternative: use the equivalent result in modular representation theory
 transitivity #|@socle_of_Iirr _ G @^-1: linear_irr _|; last first.
@@ -2476,7 +2476,7 @@ Qed.
 
 (* A combinatorial group isommorphic to the linear characters. *)
 Lemma lin_char_group G :
-  {linG : finGroupType & {cF : linG -> 'CF(G) | 
+  {linG : finGroupType & {cF : linG -> 'CF(G) |
          [/\ injective cF, #|linG| = #|G : G^`(1)|,
              forall u, cF u \is a linear_char
            & forall phi, phi \is a linear_char -> exists u, phi = cF u]
@@ -2539,7 +2539,7 @@ by rewrite !h'K Dj o_h hX generator_coprime coprime_sym in gen_j *; exists k.
 Qed.
 
 (* This is Isaacs (2.24). *)
-Lemma card_subcent1_coset G H x : 
+Lemma card_subcent1_coset G H x :
   x \in G -> H <| G -> (#|'C_(G / H)[coset H x]| <= #|'C_G[x]|)%N.
 Proof.
 move=> Gx nsHG; rewrite -leC_nat.
@@ -2705,7 +2705,7 @@ Qed.
 
 End CfDetOps.
 
-Definition cfcenter (gT : finGroupType) (G : {set gT}) (phi : 'CF(G)) := 
+Definition cfcenter (gT : finGroupType) (G : {set gT}) (phi : 'CF(G)) :=
   if phi \is a character then [set g in G | `|phi g| == phi 1%g] else cfker phi.
 
 Notation "''Z' ( phi )" := (cfcenter phi) : cfun_scope.
@@ -2716,7 +2716,7 @@ Variable (gT : finGroupType) (G : {group gT}).
 Implicit Types (phi chi : 'CF(G)) (H : {group gT}).
 
 (* This is Isaacs (2.27)(a). *)
-Lemma cfcenter_repr n (rG : mx_representation algCF G n) : 
+Lemma cfcenter_repr n (rG : mx_representation algCF G n) :
   'Z(cfRepr rG)%CF = rcenter rG.
 Proof.
 rewrite /cfcenter /rcenter cfRepr_char /=.
@@ -2813,7 +2813,7 @@ exact/quo_mx_irr.
 Qed.
 
 (* This is Isaacs (2.27)(e). *)
-Lemma cfcenter_subset_center chi : 
+Lemma cfcenter_subset_center chi :
   ('Z(chi)%CF / cfker chi)%g \subset 'Z(G / cfker chi)%g.
 Proof.
 case Nchi: (chi \is a character); last first.
@@ -2826,7 +2826,7 @@ by rewrite !mulmxA !repr_mxKV.
 Qed.
 
 (* This is Isaacs (2.27)(f). *)
-Lemma cfcenter_eq_center (i : Iirr G) : 
+Lemma cfcenter_eq_center (i : Iirr G) :
   ('Z('chi_i)%CF / cfker 'chi_i)%g = 'Z(G / cfker 'chi_i)%g.
 Proof.
 apply/eqP; rewrite eqEsubset; rewrite cfcenter_subset_center ?irr_char //.
@@ -2883,7 +2883,7 @@ congr (_ <= _ ?= iff _): (cfnorm_Res_leif 'chi_i (cfcenter_sub 'chi_i)).
   by rewrite mulr1 irr1_degree conjC_nat.
 by rewrite cfdot_irr eqxx mulr1.
 Qed.
-  
+
 (* This is Isaacs (2.31). *)
 Lemma irr1_abelian_bound (i : Iirr G) :
   abelian (G / 'Z('chi_i)%CF) -> ('chi_i 1%g) ^+ 2 = #|G : 'Z('chi_i)%CF|%:R.
@@ -2920,7 +2920,7 @@ by rewrite -injm_center; first apply: injm_morphim_inj; rewrite ?norms1.
 Qed.
 
 (* This is Isaacs (2.32)(b). *)
-Lemma pgroup_cyclic_faithful (p : nat) :  
+Lemma pgroup_cyclic_faithful (p : nat) :
   p.-group G -> cyclic 'Z(G) -> exists i, cfaithful 'chi[G]_i.
 Proof.
 pose Z := 'Ohm_1('Z(G)) => pG cycZG; have nilG := pgroup_nil pG.
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 54ed564b86..ea99f65188 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -1906,7 +1906,7 @@ rewrite eqn_dvd dvdn_exponent //= -ltnNge => lt_x_e.
 rewrite (leq_trans (ltn_Pmull (prime_gt1 p_pr) _)) ?expn_gt0 ?prime_gt0 //.
 rewrite -expnS dvdn_leq // ?gcdn_gt0 ?order_gt0 // dvdn_gcd.
 rewrite pfactor_dvdn // dvdn_exp2l.
-  by rewrite -[xp in _ < xp]subn0 ltn_sub2l // lognE p_pr order_gt0 p_dv_x.
+  by rewrite -[ltnRHS]subn0 ltn_sub2l // lognE p_pr order_gt0 p_dv_x.
 rewrite ltn_sub2r // ltnNge -(dvdn_Pexp2l _ _ (prime_gt1 p_pr)) -!p_part.
 by rewrite !part_pnat_id // (pnat_dvd (exponent_dvdn G)).
 Qed.
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index aca1a29d3e..db0d4d72bb 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -138,10 +138,10 @@ Lemma ltn_pmod m d : 0 < d -> m %% d < d.
 Proof. by rewrite ltn_mod. Qed.
 
 Lemma leq_trunc_div m d : m %/ d * d <= m.
-Proof. by rewrite [m in _ <= m](divn_eq m d) leq_addr. Qed.
+Proof. by rewrite [leqRHS](divn_eq m d) leq_addr. Qed.
 
-Lemma leq_mod m d : m %% d  <= m.
-Proof. by rewrite [m in _ <= m](divn_eq m d) leq_addl. Qed.
+Lemma leq_mod m d : m %% sd  <= m.
+Proof. by rewrite [leqRHS](divn_eq m d) leq_addl. Qed.
 
 Lemma leq_div m d : m %/ d <= m.
 Proof.
@@ -613,7 +613,7 @@ elim/ltn_ind: m n => -[|m] IHm [|n] //=.
 rewrite gcdnE; case def_p: (_ %% _) => [|p]; first by rewrite /dvdn def_p.
 have lt_pm: p < m by rewrite -ltnS -def_p ltn_pmod.
 rewrite /= (divn_eq n.+1 m.+1) def_p dvdn_addr ?dvdn_mull //; last exact: IHm.
-by rewrite gcdnE /= IHm // (ltn_trans (ltn_pmod _ _)). 
+by rewrite gcdnE /= IHm // (ltn_trans (ltn_pmod _ _)).
 Qed.
 
 Lemma dvdn_gcdl m n : gcdn m n %| m.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 39b9a8e6be..a87a638c45 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -38,8 +38,8 @@ From mathcomp Require Import ssreflect ssrfun ssrbool.
 (*         x != y :> T <=> x and y compare unequal at type T.                 *)
 (*             x =P y  :: a proof of reflect (x = y) (x == y); x =P y coerces *)
 (*                     to x == y -> x = y.                                    *)
-(*               eqLHS := (X in (X == _))%pattern (for rewriting)             *)
-(*               eqRHS := (X in (_ == X))%pattern (for rewriting)             *)
+(*              eqbLHS := (X in (X == _))%pattern (for rewriting)             *)
+(*              eqbRHS := (X in (_ == X))%pattern (for rewriting)             *)
 (*               eq_op == the boolean relation behind the == notation.        *)
 (*             pred1 a == the singleton predicate [pred x | x == a].          *)
 (* pred2, pred3, pred4 == pair, triple, quad predicates.                      *)
@@ -191,8 +191,8 @@ Notation "x =P y" := (eqP : reflect (x = y) (x == y))
 Notation "x =P y :> T" := (eqP : reflect (x = y :> T) (x == y :> T))
   (at level 70, y at next level, no associativity) : eq_scope.
 
-Notation eqLHS := (X in (X == _))%pattern.
-Notation eqRHS := (X in (_ == X))%pattern.
+Notation eqbLHS := (X in (X == _))%pattern.
+Notation eqbRHS := (X in (_ == X))%pattern.
 
 Prenex Implicits eq_op eqP.
 
diff --git a/mathcomp/ssreflect/order.v b/mathcomp/ssreflect/order.v
index 3829757cdb..6701b05edc 100644
--- a/mathcomp/ssreflect/order.v
+++ b/mathcomp/ssreflect/order.v
@@ -8488,7 +8488,7 @@ Proof.
 pose sum p := \sum_(i < n | (i < tag p)%N) p_ i + tagged p.
 rewrite -/(sum _); have sumlt : forall p, (sum p < \sum_i p_ i)%N.
   rewrite /sum => -[/= i j].
-  rewrite [X in (_ < X)%N](bigID [pred i' : 'I__ | (i' < i)%N])/= ltn_add2l.
+  rewrite [ltnRHS](bigID [pred i' : 'I__ | (i' < i)%N])/= ltn_add2l.
   by rewrite (bigD1 i) ?ltnn//= ltn_addr.
 suff: rank =1 (fun p => Ordinal (sumlt p)) by move=> /(_ p)/(congr1 val).
 apply: (Order.mono_unique _ _ le_rank) => //=.
@@ -8499,10 +8499,10 @@ case: (ltngtP i i') => //= [ltii' _|/val_inj ii']; last first.
   by rewrite -ii' in j' *; rewrite tagged_asE => ltjj'; rewrite ltn_add2l.
 rewrite ltn_addr// (@leq_trans (\sum_(i0 < n | (i0 < i)%N) p_ i0 + p_ i))%N//.
   by rewrite ltn_add2l.
-rewrite [X in (_ <= X)%N](bigID [pred i' : 'I__ | (i' < i)%N])/=.
+rewrite [leqRHS](bigID [pred i' : 'I__ | (i' < i)%N])/=.
 rewrite leq_add//; last first.
   by rewrite (bigD1 i) ?ltnn ?ltii'//= leq_addr.
-rewrite [X in (_ <= X)%N](eq_bigl [pred k : 'I_n | (k < i)%N])// => k/=.
+rewrite [leqRHS](eq_bigl [pred k : 'I_n | (k < i)%N])// => k/=.
 by case: (ltnP k i); rewrite ?andbF// => /ltn_trans->.
 Qed.
 
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 4c47eaa9de..b7aa590f32 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -165,7 +165,7 @@ Definition pi_of (n : pi_arg) : nat_pred := [pred p in primes n].
 
 Notation "\pi ( n )" := (pi_of n)
   (at level 2, format "\pi ( n )") : nat_scope.
-Notation "\p 'i' ( A )" := \pi(#|A|) 
+Notation "\p 'i' ( A )" := \pi(#|A|)
   (at level 2, format "\p 'i' ( A )") : nat_scope.
 
 Definition pdiv n := head 1 (primes n).
@@ -301,7 +301,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 -[p in p < _]muln1 ltn_pmul2l.
+  - by rewrite -[ltnLHS]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.
@@ -322,14 +322,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 -[q in q < _]muln1 ltn_pmul2l //.
+  have lt0q := ltnW lt1q; rewrite lt1q -[ltnLHS]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 -[q in q < _]mul1n ltn_mul // -[q.+1]muln1 leq_mul.
+  by rewrite lt1q -[ltnLHS]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.
@@ -423,7 +423,7 @@ by rewrite Gauss_dvdr // prime_coprime // dv_pm.
 Qed.
 
 Lemma Euclid_dvd_prod (I : Type) (r : seq I) (P : pred I) (f : I -> nat) p :
-  prime p ->  
+  prime p ->
   p %| \prod_(i <- r | P i) f i = \big[orb/false]_(i <- r | P i) (p %| f i).
 Proof.
 move=> pP; apply: big_morph=> [x y|]; [exact: Euclid_dvdM | exact: Euclid_dvd1].
@@ -530,8 +530,8 @@ 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.
 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.
+rewrite -leqNgt [leqRHS]def_q leq_pmul2r // pdiv_min_dvd //.
+  by rewrite -[pdiv n]mul1n [ltnRHS]def_q ltn_pmul2r in lt_pm_m.
 by rewrite def_q dvdn_mulr.
 Qed.
 
@@ -541,7 +541,7 @@ 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 -[n in n < _]muln1 ltn_pmul2l ?prime_gt1 ?prime_gt0.
+  by rewrite leqNgt -[ltnLHS]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 => // /ltn_pdiv2_prime -> //; exact: ltnW.
@@ -842,7 +842,7 @@ case: trunc_log => [//|k] b1 b2.
 apply/idP/idP => [/eqP sk0 | nlep]; first by move: b2; rewrite sk0.
 symmetry; rewrite -[_ == _]/false /is_true -b1; apply/negbTE; rewrite -ltnNge.
 move: nlep; rewrite -ltnS => nlep; apply: (leq_ltn_trans nlep).
-by rewrite -[X in X <= _]expn1; apply: leq_pexp2l.
+by rewrite -[leqLHS]expn1; apply: leq_pexp2l.
 Qed.
 
 Lemma trunc_log_gt0 p n : (0 < trunc_log p n) = (1 < p) && (p.-1 < n).
@@ -901,7 +901,7 @@ Qed.
 (* Truncated up real logarithm *)
 
 Definition up_log p n :=
-  if (p <= 1) then 0 else 
+  if (p <= 1) then 0 else
   let v := trunc_log p n in if n <= p ^ v then v else v.+1.
 
 Lemma up_log0 p : up_log p 0 = 0.
@@ -992,7 +992,7 @@ Proof.
 case: n=> // [] [|n] // _.
 apply: up_log_eq => //; apply/andP; split.
   apply: leq_trans (_ : n./2.+1.*2 < n.+3); last first.
-    by rewrite doubleS !ltnS -[X in _ <= X]odd_double_half leq_addl.
+    by rewrite doubleS !ltnS -[leqRHS]odd_double_half leq_addl.
   have /= /andP[H1n _] := up_log_bounds (isT : 1 < 2) (isT : 1 < n./2.+2).
   by rewrite ltnS -leq_double -mul2n -expnS prednK ?up_log_gt0 // in H1n.
 rewrite -[_./2.+1]/(n./2.+2).
@@ -1000,7 +1000,7 @@ have /= /andP[_ H2n] := up_log_bounds (isT : 1 < 2) (isT : 1 < n./2.+2).
 rewrite -leq_double -!mul2n -expnS in H2n.
 apply: leq_trans H2n.
 rewrite mul2n !doubleS !ltnS.
-by rewrite -[X in X <= _]odd_double_half -add1n leq_add2r; case: odd.
+by rewrite -[leqLHS]odd_double_half -add1n leq_add2r; case: odd.
 Qed.
 
 Lemma up_log_trunc_log p n :
@@ -1201,7 +1201,7 @@ Proof.
 case p_pr: (prime p); first by rewrite p_part pfactorK.
 by rewrite lognE (lognE p m) p_pr.
 Qed.
-    
+
 Lemma partn_lcm pi m n : m > 0 -> n > 0 -> (lcmn m n)`_pi = lcmn m`_pi n`_pi.
 Proof.
 move=> m_gt0 n_gt0; have p_gt0: lcmn m n > 0 by rewrite lcmn_gt0 m_gt0.
@@ -1419,10 +1419,10 @@ Lemma pi'_p'nat pi p n : pi^'.-nat n -> p \in pi -> p^'.-nat n.
 Proof.
 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.
 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.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index 390b3037af..da62a952c9 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -53,6 +53,12 @@ Require Export Ring.
 (*   the size of the library down. All the inequalities refer to the same     *)
 (*   constant "leq"; in particular m < n is identical to m.+1 <= n.           *)
 (*                                                                            *)
+(* -> patterns for contextual rewriting:                                      *)
+(*      leqLHS := (X in (X <= _)%N)%pattern                                   *)
+(*      leqRHS := (X in (_ <= RHS)%N)%pattern                                 *)
+(*      ltnLHS := (X in (X < _)%N)%pattern                                    *)
+(*      ltnRHS := (X in (_ < X)%N)%pattern                                    *)
+(*                                                                            *)
 (*   conditionally strict inequality `leqif'                                  *)
 (*      m <= n ?= iff condition   ==   (m <= n) and ((m == n) = condition)    *)
 (*   This is actually a pair of boolean equalities, so rewriting with an      *)
@@ -856,6 +862,11 @@ Proof.
 by have [le_nm|/eqnP-> //] := leqP; rewrite -{1}(subnK le_nm) -addSn addnK.
 Qed.
 
+Notation leqLHS := (X in (X <= _)%N)%pattern.
+Notation leqRHS := (X in (_ <= X)%N)%pattern.
+Notation ltnLHS := (X in (X < _)%N)%pattern.
+Notation ltnRHS := (X in (_ < X)%N)%pattern.
+
 (* Getting a concrete value from an abstract existence proof. *)
 
 Section ExMinn.
@@ -1106,7 +1117,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 -[m in m < _]mul1n ltn_pmul2r. Qed.
+Proof. by move=> lt1n m_gt0; rewrite -[ltnLHS]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.

From 68073e16e4bc41625d25cad6642dc2f6fad86f22 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 29 Apr 2022 08:26:16 +0900
Subject: [PATCH 3/3] fix

---
 mathcomp/ssreflect/div.v    | 2 +-
 mathcomp/ssreflect/ssrnat.v | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index db0d4d72bb..66f650e047 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -140,7 +140,7 @@ Proof. by rewrite ltn_mod. Qed.
 Lemma leq_trunc_div m d : m %/ d * d <= m.
 Proof. by rewrite [leqRHS](divn_eq m d) leq_addr. Qed.
 
-Lemma leq_mod m d : m %% sd  <= m.
+Lemma leq_mod m d : m %% d <= m.
 Proof. by rewrite [leqRHS](divn_eq m d) leq_addl. Qed.
 
 Lemma leq_div m d : m %/ d <= m.
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index da62a952c9..34d91171ca 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -55,7 +55,7 @@ Require Export Ring.
 (*                                                                            *)
 (* -> patterns for contextual rewriting:                                      *)
 (*      leqLHS := (X in (X <= _)%N)%pattern                                   *)
-(*      leqRHS := (X in (_ <= RHS)%N)%pattern                                 *)
+(*      leqRHS := (X in (_ <= X)%N)%pattern                                   *)
 (*      ltnLHS := (X in (X < _)%N)%pattern                                    *)
 (*      ltnRHS := (X in (_ < X)%N)%pattern                                    *)
 (*                                                                            *)