diff --git a/probability/convex_stone.v b/probability/convex_stone.v
index 4e1ced31..c5bba52a 100644
--- a/probability/convex_stone.v
+++ b/probability/convex_stone.v
@@ -804,7 +804,7 @@ case/boolP : (d ord0 == 0 :> R)%coqR => d00.
 have H : [p_of p.~%:pr, (probfdist d ord0).~%:pr] != 1%coqR%:pr.
   apply p_of_neq1 => /=; split.
     apply/RltP/onem_gt0; rewrite -fdist_lt1; exact/eqP.
-  by apply/RltP; rewrite ltr_subl_addr ltr_addl -fdist_gt0.
+  by apply/RltP; rewrite ltrBlDr ltrDl -fdist_gt0.
 rewrite -convA'; last by [].
 move=> [:Hq].
 have @q : {prob R}.
@@ -814,9 +814,9 @@ have @q : {prob R}.
   rewrite !fdistI_permE !permE /= (_ : Ordinal _ = ord_max); last exact/val_inj.
   apply/andP. split.
     apply/divr_ge0 => //; first by apply/ltW; rewrite subr_gt0 -fdist_lt1.
-  rewrite ler_pdivr_mulr ?mul1r; last by rewrite subr_gt0 -fdist_lt1 //.
-  rewrite ler_subr_addr -(FDist.f1 d) !big_ord_recl big_ord0 addr0.
-  by rewrite (_ : lift _ (lift _ _) = ord_max) ?ler_addr //; exact/val_inj.
+  rewrite ler_pdivrMr ?mul1r; last by rewrite subr_gt0 -fdist_lt1 //.
+  rewrite lerBrDr -(FDist.f1 d) !big_ord_recl big_ord0 addr0.
+  by rewrite (_ : lift _ (lift _ _) = ord_max) ?lerDr //; exact/val_inj.
 rewrite (@convn3E _ _ q) //; last first.
   rewrite fdistI_permE permE /= (_ : Ordinal _ = ord_max) //; exact/val_inj.
 rewrite /= !permE /=.
@@ -1017,10 +1017,10 @@ have @q : {prob R}.
   abstract: Hq.
   apply/andP. split.
     by apply/divr_ge0/ltW => //; rewrite subr_gt0 -fdist_lt1.
-  rewrite ler_pdivr_mulr.
+  rewrite ler_pdivrMr.
     rewrite mul1r.
-    rewrite ler_subr_addr -(FDist.f1 d).
-    rewrite 2!big_ord_recl addrA ler_addl.
+    rewrite lerBrDr -(FDist.f1 d).
+    rewrite 2!big_ord_recl addrA lerDl.
     by apply: sumr_ge0 => i _.
   by rewrite subr_gt0 -fdist_lt1.
 rewrite (@convn3E _ _ q); last 2 first.