Revert "Fix for math-comp/math-comp#399"

This reverts commit 050fb63.
math-comp · Nov 15, 2019 · 4ff7841 · 4ff7841
1 parent 050fb63
commit 4ff7841
Show file tree

Hide file tree

Showing 4 changed files with 5 additions and 5 deletions.
diff --git a/theories/BGsection2.v b/theories/BGsection2.v
@@ -539,7 +539,7 @@ case: (leqP k j.+1) => [ | lt_j1_k].
 case: (leqP h.-1 (k - j)) => [le_h1_kj | lt_kj_h1].
   have k_h1: k = h.-1.
     apply/eqP; rewrite eqn_leq -ltnS (prednK h_gt0) lt_kh.
-    exact: leq_trans (leq_subl j k).
+    exact: leq_trans (leq_subr j k).
   have j0: j = 0%N.
     apply/eqP; rewrite -leqn0 -(leq_add2l k) -{2}(subnK (ltnW lt_jk)).
     by rewrite addn0 leq_add2r {1}k_h1.

diff --git a/theories/PFsection10.v b/theories/PFsection10.v
@@ -763,7 +763,7 @@ have ub_G1: #|G1|%:R / #|G|%:R <= #|H|%:R / #|S|%:R + #|V|%:R / #|W|%:R :> algC.
   rewrite ler_pdivr_mulr ?ltr0n ?cardG_gt0 // mulrC mulrDr !mulrA.
   rewrite ![_ * _ / _]mulrAC -!natf_indexg ?subsetT //= -!natrM -natrD ler_nat.
   apply: leq_trans (subset_leq_card sG1_HVG) _.
-  rewrite cardsU (leq_trans (leq_subl _ _)) //.
+  rewrite cardsU (leq_trans (leq_subr _ _)) //.
   have unifJG B C: C \in B :^: G -> #|C| = #|B|.
     by case/imsetP=> z _ ->; rewrite cardJg.
   have oTI := card_uniform_partition (unifJG _) (partition_class_support _ _).

diff --git a/theories/PFsection13.v b/theories/PFsection13.v
@@ -1203,7 +1203,7 @@ have lb_m r b d: test r.+2 b d -> (q >= r.+2)%N -> m > b%:R / d%:R.
     by rewrite leC_nat -ltnS (ltn_predK qgt2).
   rewrite -(ltn_predK pgt2) expnSr natrM invfM mulrA.
   rewrite ler_pdivr_mulr ?gt0CG // mulrAC mul1r -subn1.
-  rewrite ler_pmul ?invr_ge0 ?ler0n ?leC_nat ?leq_subl //.
+  rewrite ler_pmul ?invr_ge0 ?ler0n ?leC_nat ?leq_subr //.
   rewrite lef_pinv ?qualifE ?ltr0n ?leC_nat ?expn_gt0 ?(prime_gt0 pr_q) //.
   apply: leq_trans (_ : q ^ 2 <= _)%N; first by rewrite leq_exp2r.
   by rewrite -(subnKC qgt2) leq_pexp2l // -subn1 ltn_subRL.

diff --git a/theories/PFsection14.v b/theories/PFsection14.v
@@ -171,7 +171,7 @@ have ->: (u * q)%:R^-1 = #|S|%:R^-1 * #|P|%:R :> algC.
 have [_ _] := FTtypeII_ker_TI maxS Stype2; rewrite FTsupp1_type2 // => tiP1.
 rewrite {tiP1}(card_support_normedTI tiP1) natrM natf_indexg ?subsetT //.
 rewrite mulrCA mulKf ?neq0CG // mulrC ler_pmul2l ?invr_gt0 ?gt0CG // leC_nat.
-by rewrite cardsDS ?sub1G ?leq_subl.
+by rewrite cardsDS ?sub1G ?leq_subr.
 Qed.
 
 Hypotheses (maxNU_L : L \in 'M('N(U))) (phi1 : phi 1%g = e%:R).
@@ -709,7 +709,7 @@ rewrite -mulnA leq_mul // mulnA mulnCA mulnC leq_mul // -bin_sub ?leqW //.
 rewrite -(leq_pmul2r (fact_gt0 (q.+1 - i))) -mulnA bin_ffact mulnC subSn //.
 rewrite ffactnS /= -!mulnA leq_mul //=; elim: {i leiq}(q - i)%N => //= i IHi.
 rewrite ffactnSr expnSr mulnACA expnS factS (mulnACA n) mulnC leq_mul //.
-by rewrite leq_mul // (leq_trans (leq_subl _ _)).
+by rewrite leq_mul // (leq_trans (leq_subr _ _)).
 Qed.
 
 (* This is Peterfalvi (14.8)(b). *)