Merge pull request #55 from coq-community/mc_1190

Adapt to math-comp/math-comp#1190

.github/workflows/docker-action.yml

@@ -23,6 +23,11 @@ jobs:
           - 'mathcomp/mathcomp:2.0.0-coq-8.18'
           - 'mathcomp/mathcomp:2.1.0-coq-8.16'
           - 'mathcomp/mathcomp:2.1.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.2.0-coq-dev'
+          - 'mathcomp/mathcomp-dev:coq-8.17'
+          - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:

README.md

@@ -9,8 +9,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [![Code of Conduct][conduct-shield]][conduct-link]
 [![Zulip][zulip-shield]][zulip-link]
 
-[docker-action-shield]: https://github.com/coq-community/fourcolor/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/coq-community/fourcolor/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/coq-community/fourcolor/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/coq-community/fourcolor/actions/workflows/docker-action.yml
 
 [contributing-shield]: https://img.shields.io/badge/contributions-welcome-%23f7931e.svg
 [contributing-link]: https://github.com/coq-community/manifesto/blob/master/CONTRIBUTING.md

coq-fourcolor.opam

@@ -20,8 +20,8 @@ basic plane topology definitions, and a theory of combinatorial hypermaps."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {(>= "8.16" & < "8.19~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {(>= "2.0.0" & < "2.2~") | (= "dev")}
+  "coq" {(>= "8.16" & < "8.20~") | (= "dev")}
+  "coq-mathcomp-ssreflect" {(>= "2.0.0" & < "2.3~") | (= "dev")}
   "coq-mathcomp-algebra" 
 ]
 

meta.yml

@@ -35,7 +35,7 @@ license:
 
 supported_coq_versions:
   text: 8.16 or later
-  opam: '{(>= "8.16" & < "8.19~") | (= "dev")}'
+  opam: '{(>= "8.16" & < "8.20~") | (= "dev")}'
 
 tested_coq_opam_versions:
 - version: '2.0.0-coq-8.16'
@@ -46,6 +46,16 @@ tested_coq_opam_versions:
   repo: 'mathcomp/mathcomp'
 - version: '2.1.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
+- version: '2.2.0-coq-8.16'
+  repo: 'mathcomp/mathcomp'
+- version: '2.2.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '2.2.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
+- version: 'coq-8.17'
+  repo: 'mathcomp/mathcomp-dev'
+- version: 'coq-8.19'
+  repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
 
@@ -56,7 +66,7 @@ ci_cron_schedule: '0 5 * * *'
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{(>= "2.0.0" & < "2.2~") | (= "dev")}'
+    version: '{(>= "2.0.0" & < "2.3~") | (= "dev")}'
   description: |-
     [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
 - opam:

theories/approx.v

@@ -266,11 +266,11 @@ have [nx1 lbx1 ubx1] := approx_between Dmx Dmx1 (scale_s_dxy (i4 1%N isT)).
 have [ny0 lby0 uby0] := approx_between Dmy0 Dmy (scale_s_dxy (i4 2%N isT)).
 have [ny1 lby1 uby1] := approx_between Dmy Dmy1 (scale_s_dxy (i4 3%N isT)).
 exists (s1, Grect nx0 (nx1 + 1) ny0 (ny1 + 1)) => /=.
-  by exists (Gpoint mx my); rewrite //= !addrK -!lez_addr1 ubx0 lbx1 uby0 lby1.
+  by exists (Gpoint mx my); rewrite //= !addrK -!lezD1 ubx0 lbx1 uby0 lby1.
 have lt_approx u v mu mv: ap_s1 u mu -> ap_s1 v mv -> (mu + 1 <= mv)%R -> u < v.
   case=> _ ubu [lbv _] ltuv; apply/(leR_pmul2l v u es1gt0)/(ltR_le_trans ubu).
   by apply: leR_trans lbv; rewrite -intRD1; apply/intR_leP.
-case=> x2 y2 [[mx2 my2] [Dmx2 Dmy2]] /=; rewrite -andbA -!lez_addr1 => /and4P[].
+case=> x2 y2 [[mx2 my2] [Dmx2 Dmy2]] /=; rewrite -andbA -!lezD1 => /and4P[].
 move=> /(le_trans lbx0)/lt_approx-lbx /le_trans/(_ ubx1)/lt_approx-ubx.
 move=> /(le_trans lby0)/lt_approx-lby /le_trans/(_ uby1)/lt_approx-uby.
 by do 2!split; [apply/lbx | apply/ubx | apply/lby | apply/uby].
@@ -291,7 +291,7 @@ rewrite -(leR_pmul2l _ x1 sXgt0) -(leR_pmul2l x1 _ sXgt0) !sZK => lbx1 ubx1 [].
 rewrite -(leR_pmul2l _ y1 sXgt0) -(leR_pmul2l y1 _ sXgt0) !sZK => lby1 uby1.
 have [p1 Dp1] := approx_point_exists s (Point x1 y1); exists p1 => //.
 case: p1 Dp1 => [p1x p1y] [[ubp1x lbp1x] [ubp1y lbp1y]] /=.
-rewrite -!(rwP andP) -!ltz_addr1 -!lez_addr1 -!(rwP (@intR_ltP R _ _)).
+rewrite -!(rwP andP) -!ltzD1 -!lezD1 -!(rwP (@intR_ltP R _ _)).
 rewrite (intRD1 R p1x) (intRD1 R p1y)  -/intRR; split.
   by split; [apply: ltR_trans lbp1x | apply: leR_lt_trans ubx1].
 by split; [apply: ltR_trans lbp1y | apply: leR_lt_trans uby1].

theories/cfmap.v

@@ -507,7 +507,7 @@ HB.instance Definition _ (A : choiceType) := Choice.copy (ecp_dart A)
 HB.instance Definition _ (A : countType) := Countable.copy (ecp_dart A)
   (can_type (@ecp_cancel A)).
 HB.instance Definition _ (A : finType) : isFinite (ecp_dart A) :=
-  CanFinMixin (@ecp_cancel A).
+  CanIsFinite (@ecp_cancel A).
 
 Lemma card_ecp (A : finType) : #|ecp_dart A| = #|A|.+2.
 Proof.

theories/chromogram.v

@@ -72,7 +72,7 @@ Proof. by do 2!case; constructor. Qed.
 HB.instance Definition _ := hasDecEq.Build gram_symbol eqgsP.
 
 Definition chromogram : predArgType := seq gram_symbol.
-Canonical chromogram_eqType := [eqType of chromogram].
+HB.instance Definition _ := Equality.on chromogram.
 
 Fixpoint gram_balanced d b0 (w : chromogram) {struct w} :=
   match w, d with

theories/color.v

@@ -214,7 +214,7 @@ Proof. by case: c => // _ []. Qed.
 (* Boolean correctness predicate *)
 
 Definition colseq : predArgType := seq color.
-Canonical colseq_eqType := [eqType of colseq].
+HB.instance Definition _ := Equality.on colseq.
 
 Definition head_color : colseq -> color := head Color0.
 

theories/coloring.v

@@ -241,7 +241,7 @@ have nnx: node (node x) = x.
   rewrite (cardD1 x) (cardD1 (node x)) (cardD1 (node (node x))) !inE.
   by rewrite (inj_eq nodeI) x'nx x'n2x -!cnode1r connect0.
 pose G' := WalkupE x; pose h' (u : G') := val u.
-pose unx : G' := sub (node x) x'nx; pose G'' := WalkupE unx.
+pose unx : G' := Sub (node x) x'nx; pose G'' := WalkupE unx.
 pose h'' (w : G'') := val w; pose h := h' (h'' _).
 have Ih': injective h' := val_inj; have Ih'': injective h'' := val_inj.
 have Ih: injective h := inj_comp Ih' Ih''.
@@ -262,7 +262,7 @@ have oE_G'' w: order edge w = #|predD1 (cedge (h'' w)) unx|.
   rewrite /order -(card_image Ih''); apply: eq_card => u; rewrite inE /=.
   have [u_nx | nx'u] := altP eqP.
     by apply/imageP => [[wu _ u_wu]]; case/eqP: (valP wu); rewrite -[RHS]u_nx.
-  set wu : G'' := sub u nx'u; rewrite (mem_image Ih'' _ wu) /=.
+  set wu : G'' := Sub u nx'u; rewrite (mem_image Ih'' _ wu) /=.
   apply: etrans (eq_fconnect (glink_fp_skip_edge _) w wu) _.
     by rewrite /glink /= -!val_eqE /= nnx !eqxx /= orbT.
   exact: (fconnect_skip edgeI w wu).
@@ -280,7 +280,7 @@ have [|k [kE kF]] := minimal_counter_example_is_minimal cexG _ ltG''G.
     have [/negPf Eu'x Eu'nx] := norP Eu'Nx; rewrite /= orbF in Eu'nx.
     apply/eqP; apply: eq_card => y.
     have [-> {y} | x'y] := eqVneq y x; last first.
-      pose v : G' := sub y x'y; rewrite (mem_image Ih' _ v) !inE.
+      pose v : G' := Sub y x'y; rewrite (mem_image Ih' _ v) !inE.
       case: eqP => [[ynx] | _]; last exact (same_cskip_edge Eu'Nx).
       by apply/esym/(contraNF _ Eu'nx) => wEy; rewrite /= -ynx.
     rewrite [x \in cedge _]Eu'x; apply/imageP=> [[[z x'z] _ /= zx]].
@@ -300,13 +300,13 @@ have [|k [kE kF]] := minimal_counter_example_is_minimal cexG _ ltG''G.
   rewrite (cardD1 x) !inE connect0 eqSS /order -(card_image Ih').
   apply/eqP/esym/eq_card => y; rewrite !inE; have [-> | x'y] /= := altP eqP.
     by apply/imageP=> [[[z x'z] _ /esym/eqP/idPn]].
-  set v : G' := sub y x'y; rewrite (mem_image Ih' _ v).
+  set v : G' := Sub y x'y; rewrite (mem_image Ih' _ v).
   by apply: (etrans (cskip_edge_merge x'Enx EuNx)); rewrite /= orbF !(cedgeC y).
 case: (minimal_counter_example_is_noncolorable cexG).
 pose a' x w := cface x (h w).
 have a'0P y: a' y =1 pred0 -> pred2 x (node x) y.
-  move=> a'y0; apply/norP => [[x'y nx'y]]; pose uy : G' := sub y x'y.
-  by case/idP: (a'y0 ((sub uy : _ -> G'') nx'y)); apply: connect0.
+  move=> a'y0; apply/norP => [[x'y nx'y]]; pose uy : G' := Sub y x'y.
+  by case/idP: (a'y0 ((Sub uy : _ -> G'') nx'y)); apply: connect0.
 have a'F y z: a' y =1 pred0 -> cface y z -> y = z.
   move=> a'y0 yFz; suffices: pred2 y (node y) z.
     by case/pred2P=> // zny; rewrite -[y]nodeK -zny -cface1 cfaceC F'eG in yFz.
@@ -323,7 +323,7 @@ have k'F y z: cface y z -> k' y = k' z.
   rewrite /a' (same_cface yFz) in yFw; case: pickP => [w' zFw' | /(_ w)/idP//].
   by apply: kFF; rewrite hF -(same_cface yFw).
 have k'E y: ~~ (pred2 x (node x) y) -> k' y != k' (edge y).
-  case/norP=> [x'y nx'y]; pose w := (sub (sub y x'y : G') : _ -> G'') nx'y.
+  case/norP=> [x'y nx'y]; pose w := (Sub (Sub y x'y : G') : _ -> G'') nx'y.
   have Dfey: (face (edge y) = h (face (edge w))).
     by apply: nodeI; rewrite -hN1 !edgeK.
   rewrite (k'F (edge y) _ (fconnect1 _ _)) /k'.

theories/contract.v

@@ -266,14 +266,14 @@ have D_E0 (y : G0): cedge x y = (y == x) || (y == edge x).
 pose G1 := WalkupF x; pose h1 (u : G1) : G0 := val u.
 have Ih1: injective h1 by apply: val_inj.
 have x'ex: edge x != x by rewrite (plain_neq geoG0).
-pose uex : G1 := sub (edge x) x'ex.
+pose uex : G1 := Sub (edge x) x'ex.
 pose G2 := WalkupF uex; pose h2 (w : G2) : G1 := val w.
 have Ih2: injective h2 by apply: val_inj.
 pose h w := h1 (h2 w); have Ih: injective h := inj_comp Ih1 Ih2.
 have Eh: codom h =i predC (cedge x).
   move=> y; rewrite inE D_E0; apply/imageP/norP => [[w _ ->] | [x'y ex'y]].
     by rewrite (valP w) (valP (val w)).
-  by exists ((sub (sub y x'y : G1) : _ -> G2) ex'y).
+  by exists ((Sub (Sub y x'y : G1) : _ -> G2) ex'y).
 have xE'h w: cedge x (h w) = false.
   by apply: negPf; rewrite -[~~ _]Eh codom_f.
 have hN w w': cnode w w' = cnode (h w) (h w') by rewrite !fconnect_skip.

theories/cube.v

@@ -40,8 +40,8 @@ HB.instance Definition _ := Countable.copy cube_tag (can_type cube_tag_codeK).
 Fact cube_tag_enumP : Finite.axiom cube_tag_enum. Proof. by case. Qed.
 HB.instance Definition _ := isFinite.Build cube_tag cube_tag_enumP.
 
-Definition cube_dart := cube_tag * G : Type.
-HB.instance Definition _ := Finite.copy cube_dart [finType of cube_dart].
+Definition cube_dart : Type := cube_tag * G.
+HB.instance Definition _ := Finite.on cube_dart.
 
 Let tsI : cube_tag -> G -> cube_dart := @pair _ _.
 Let tsE (u : cube_dart) : G := u.2.

theories/dedekind.v

@@ -150,7 +150,7 @@ Qed.
 Fact lt_is_cut a : is_cut {b | a < b}%R.
 Proof.
 split=> [||b c /lt_trans| b /midf_lt[ltac ltcb]]; last 2 [exact].
-- by exists (a + 1)%R; rewrite ltr_addl.
+- by exists (a + 1)%R; rewrite ltrDl.
 - by exists a; rewrite ltxx.
 by exists ((a + b) / 2%:R)%R.
 Qed.
@@ -273,11 +273,11 @@ Definition opp_cut x := {a | exists2 b, (- a < b)%R & x >= b}.
 Fact opp_is_cut x : is_cut (opp_cut x).
 Proof.
 split=> [||a b [c lt_na_c lecx] | a [b /(@open (- a)%R)[c lt_na_c ltcb] lebx]].
-- by have [a leax] := cut_lb x; exists (1 - a)%R, a; rewrite // opprB gtr_addl.
+- by have [a leax] := cut_lb x; exists (1 - a)%R, a; rewrite // opprB gtrDl.
 - have [a ltxa] := cut_ub x; exists (- a)%R => -[b ltab []].
   by apply: ltc_trans ltab; rewrite opprK.
-- by exists c; first by apply: lt_trans lt_na_c; rewrite ltr_opp2.
-by exists (- c)%R; [exists b; rewrite ?opprK | rewrite ltr_oppl].
+- by exists c; first by apply: lt_trans lt_na_c; rewrite ltrN2.
+by exists (- c)%R; [exists b; rewrite ?opprK | rewrite ltrNl].
 Qed.
 
 Definition opp x := Cut (opp_is_cut x).
@@ -299,8 +299,8 @@ Proof. by move=> IHopp IHpos x; case: (ltcP x 0) gec0_opp; auto. Qed.
 Lemma oppK x : - (- x) == x.
 Proof.
 split=> [a /open[b ltxb ltba] | a [b lt_na_b le_b_nx]].
-  by exists (- b)%R => [|[c]]; rewrite ?ltr_opp2 ?opprK => // /(ltc_trans ltxb).
-by apply/notK=> leax; case: le_b_nx; exists a; rewrite // ltr_oppl.
+  by exists (- b)%R => [|[c]]; rewrite ?ltrN2 ?opprK => // /(ltc_trans ltxb).
+by apply/notK=> leax; case: le_b_nx; exists a; rewrite // ltrNl.
 Qed.
 
 Lemma eqR_opp2 x y : opp x == opp y -> x == y.
@@ -355,9 +355,9 @@ split=> [|| a b [c ltxc ltyac] ltab | a [b ltxb /open[c ltyc ltcab]]].
   by exists (b + a)%R, a; rewrite ?addrK.
 - have [[a leax] [b /leRq-leby]] := (cut_lb x, cut_lb y).
   exists (b + a)%R => -[c ltxc /leby].
-  by rewrite ltcE ltr_subr_addr ltr_add2l => /(ltc_trans ltxc).
-- by exists c => //; apply: ltc_trans ltyac _; rewrite ltr_add2r.
-by exists (c + b)%R; [exists b; rewrite ?addrK | rewrite -ltr_subr_addr].
+  by rewrite ltcE ltrBrDr ltrD2l => /(ltc_trans ltxc).
+- by exists c => //; apply: ltc_trans ltyac _; rewrite ltrD2r.
+by exists (c + b)%R; [exists b; rewrite ?addrK | rewrite -ltrBrDr].
 
 Qed.
 
@@ -390,24 +390,24 @@ Qed.
 Lemma addN x : x - x == 0.
 Proof.
 apply eqR_sym; split=> [c [a ltxa [b lt_ac_b /leRq-lebx]] | d d_gt0].
-  by rewrite ltcE -(ltr_addr (- a)) ltr_oppl (lt_trans lt_ac_b) ?lebx.
+  by rewrite ltcE -(ltrDr (- a)) ltrNl (lt_trans lt_ac_b) ?lebx.
 have [[a ltxa] [b lebx]] := (cut_ub x, cut_lb x).
 have{a ltxa d_gt0} []: exists n, x < b + d *+ n.
   have ltab: (0 < a - b)%R by move/leRq in lebx; rewrite subr_gt0 lebx.
   pose c := ((a - b) / d)%R; have c_ge0: (0 <= c)%R by rewrite ltW ?divr_gt0.
-  exists `|numq c|%N; apply: ltc_le_trans ltxa _; rewrite -ler_subl_addl.
+  exists `|numq c|%N; apply: ltc_le_trans ltxa _; rewrite -lerBlDl.
   rewrite pmulrn gez0_abs -?ge_rat0 // -mulrzl numqE mulrAC.
-  by rewrite divfK ?gt_eqF ?ler_pmulr // ler1z -gtz0_ge1 denq_gt0.
+  by rewrite divfK ?gt_eqF ?ler_pMr // ler1z -gtz0_ge1 denq_gt0.
 elim=> [|n IHn]; rewrite ?addr0 // mulrSr => /open[a ltxa lt_a_dnd].
 have [/IHn//| le_bdn_x] := classical (x < b + d *+ n).
-by exists a => //; exists (b + d *+ n)%R; rewrite // opprB ltr_subl_addr -addrA.
+by exists a => //; exists (b + d *+ n)%R; rewrite // opprB ltrBlDr -addrA.
 Qed.
 
 Lemma add0 x : 0 + x == x.
 Proof.
 split=> [a /open[b ltxb ltba] | a [b b_gt0] ltxab].
   by exists (a - b)%R; [rewrite ltcE subr_gt0 | rewrite opprD opprK addNKr].
-by apply: ltc_trans ltxab _; rewrite gtr_addl oppr_lt0.
+by apply: ltc_trans ltxab _; rewrite gtrDl oppr_lt0.
 Qed.
 
 Lemma opp0 : - 0 == 0. Proof. by rewrite -[opp 0]add0 addN. Qed.
@@ -432,9 +432,9 @@ split=> [|| a b [c ltxc ltyac] ltab | a [b ltxb /open[c ltyc ltcab]]].
   by exists (b * a)%R, a; rewrite ?mulfK ?gt_eqF // (abs_ge0 ltxa).
 - by exists 0%R => -[a _ /abs_ge0]; rewrite mul0r ltcE ltxx.
 - exists c => //; have c_gt0: 0 < c := abs_ge0 ltxc.
-  by apply: ltc_trans ltyac _; rewrite ltr_pmul2r ?invr_gt0.
+  by apply: ltc_trans ltyac _; rewrite ltr_pM2r ?invr_gt0.
 have b_gt0: 0 < b := abs_ge0 ltxb.
-by exists (c * b)%R; first exists b; rewrite -?ltr_pdivl_mulr ?mulfK ?gt_eqF.
+by exists (c * b)%R; first exists b; rewrite -?ltr_pdivlMr ?mulfK ?gt_eqF.
 Qed.
 
 Definition amul x y := Cut (amul_is_cut x y).
@@ -463,7 +463,7 @@ Lemma amulC x y : `|x|*|y| == `|y|*|x|.
 Proof.
 without loss suffices: x y / `|y|*|x| <= `|x|*|y| by [].
 move=> b [a ltxa ltyba]; exists (b / a)%R; rewrite // invf_div mulrC divfK //.
-by rewrite gt_eqF // -(mul0r a) -ltr_pdivl_mulr (abs_ge0 ltxa, abs_ge0 ltyba).
+by rewrite gt_eqF // -(mul0r a) -ltr_pdivlMr (abs_ge0 ltxa, abs_ge0 ltyba).
 Qed.
 
 Lemma amulA x y z : `|x|*|`|y|*|z| | == `| `|x|*|y| |*|z|.
@@ -537,8 +537,8 @@ have dgt0: 0 < d by move/leR0y: lty_da1; rewrite ltcE pmulr_lgt0 ?invr_gt0.
 have cdgt0: 0 < c - d.
   by move/leR0z: ltz_cda2; rewrite ltcE pmulr_lgt0 ?invr_gt0.
 exists a; rewrite // (ge0_abs le0yz); exists (d / a)%R; last rewrite -mulrBl.
-  by apply: ltc_le_trans lty_da1 _; rewrite ler_pmul2l ?lef_pinv.
-by apply: ltc_le_trans ltz_cda2 _; rewrite ler_pmul2l ?lef_pinv.
+  by apply: ltc_le_trans lty_da1 _; rewrite ler_pM2l ?lef_pV2.
+by apply: ltc_le_trans ltz_cda2 _; rewrite ler_pM2l ?lef_pV2.
 Qed.
 
 Lemma mul1 x : 1 * x == x.
@@ -547,11 +547,11 @@ elim/opp_ind: x => [x IHx | x le0x].
   by apply eqR_opp2; rewrite -IHx mulRN.
 rewrite ge0_mul //; split=> [b /open[a ltxa ltab] | b [a [lt1a _] ltxba]].
   have a_gt0: 0 < a by apply/leRq: (a) ltxa.
-  by rewrite amulC; exists a; rewrite ge0_abs // ltcE ltr_pdivl_mulr ?mul1r.
+  by rewrite amulC; exists a; rewrite ge0_abs // ltcE ltr_pdivlMr ?mul1r.
 have a_gt0: 0 < a by apply: lt_trans lt1a.
-have b_gt0: 0 < b by rewrite ltcE -(mul0r a) -ltr_pdivl_mulr ?(abs_ge0 ltxba).
+have b_gt0: 0 < b by rewrite ltcE -(mul0r a) -ltr_pdivlMr ?(abs_ge0 ltxba).
 rewrite -[x]ge0_abs //; apply: ltc_trans ltxba _.
-by rewrite gtr_pmulr ?invf_lt1.
+by rewrite gtr_pMr ?invf_lt1.
 Qed.
 
 Lemma mul_monotony x y z : 0 <= x -> y <= z -> x * y <= x * z.
@@ -601,29 +601,29 @@ pose E z := `|x|*|z| < 1; have E_0: E 0 by rewrite /E amulC amul0.
 have supE: has_sup E.
   split; [by exists 0 | exists a^-1%R => //].
   move=> z [b ltxb [lt_z_vb _]]; apply/ltcW/(ltc_trans lt_z_vb).
-  by rewrite mul1r (ltf_pinv (abs_ge0 ltxb)) ?(gec_lt_trans _ ltxb) // => -[].
+  by rewrite mul1r (ltf_pV2 (abs_ge0 ltxb)) ?(gec_lt_trans _ ltxb) // => -[].
 have ubEy: ub E y by apply: sup_ub.
 have le0y: y >= 0 by apply/leRq/ubEy.
 rewrite ge0_mul //; split=> [b lt1b | b [c ltxc [ltybc _]]]; last first.
   have [d ltxd ltdc] := open ltxc.
   have [c_gt0 d_gt0] := (abs_ge0 ltxc, abs_ge0 ltxd).
-  suffices: (1 / c < b / c)%R by rewrite ltr_pmul2r ?invr_gt0.
+  suffices: (1 / c < b / c)%R by rewrite ltr_pM2r ?invr_gt0.
   apply: gec_lt_trans ltybc; apply/leRq/ubEy; exists d => //.
-  by rewrite !mul1r ge0_abs ltcE ?ltf_pinv // lt_gtF ?invr_gt0.
+  by rewrite !mul1r ge0_abs ltcE ?ltf_pV2 // lt_gtF ?invr_gt0.
 have lt0b: 0 < b by apply: lt_trans lt1b.
 pose e := (1 - b^-1)%R; have lt0e: 0 < e by rewrite ltcE subr_gt0 invf_lt1.
 have [c ltxc [d lt_cea_d ledx]]: x - x < a * e by rewrite addN ltcE mulr_gt0.
 have ltac: a < c := gec_lt_trans leax ltxc.
 have lt0c: 0 < c := lt_trans lt0a ltac.
 have lt0d: 0 < d.
   apply: lt_trans lt_cea_d; rewrite opprB subr_gt0 mulrBr mulr1.
-  by rewrite ltr_snsaddr // oppr_lt0 divr_gt0.
+  by rewrite ltr_nDr // oppr_lt0 divr_gt0.
 have le_y_vd: y <= d^-1%R.
   apply/sup_le_ub=> // z -[f ltxf [lt_z_vf _]]; apply/ltcW/(ltc_trans lt_z_vf).
-  by rewrite mul1r (ltf_pinv (abs_ge0 ltxf)) ?(gec_lt_trans _ ltxf) // => -[].
+  by rewrite mul1r (ltf_pV2 (abs_ge0 ltxf)) ?(gec_lt_trans _ ltxf) // => -[].
 exists c; rewrite ge0_abs //; apply: le_y_vd; rewrite ltcE.
-rewrite -invf_div ltf_pinv ?rpred_div //; apply: lt_trans lt_cea_d.
-by rewrite ltr_oppr -[c in (_ - c)%R]mulr1 ltr_subl_addl -mulrBr ltr_pmul2r.
+rewrite -invf_div ltf_pV2 ?rpred_div //; apply: lt_trans lt_cea_d.
+by rewrite ltrNr -[c in (_ - c)%R]mulr1 ltrBlDl -mulrBr ltr_pM2r.
 Qed.
 
 Definition structure := Real.Structure leR sup add 0 opp mul 1 inv.

theories/discharge.v

@@ -357,7 +357,7 @@ Proof. by rewrite sort_dbound1_eq; case: (sort_drules p r). Qed.
 
 Lemma dbound2_leq : dscore2 (face (face x)) <= dbound2 rt rs x.
 Proof.
-rewrite /dbound2 -dbound1_eq ler_add2r lez_nat.
+rewrite /dbound2 -dbound1_eq lerD2r lez_nat.
 set y := inv_face2 _; rewrite /rt /target_drules; case: rf => _ _ [].
 elim: the_drules => //= r dr IHdr; case Dr': (converse_part r) => [u r'].
 case Hyr: (exact_fitp y r).
@@ -382,10 +382,10 @@ move=> ub_m x pos_x d max_m; apply: contraLR pos_x; rewrite -leqNgt => ledx.
 have ltm10: (m < 10)%N by rewrite -subn_gt0; case: (10 - m)%N max_m.
 have{max_m}: 60%:Z <= ((10 - m) * arity x)%:Z.
   by rewrite lez_nat (leq_trans max_m) ?leq_mul.
-rewrite -leNgt -ler_subr_addr ler_subl_addl add0r => /le_trans-> //.
+rewrite -leNgt -lerBrDr lerBlDl add0r => /le_trans-> //.
 rewrite !PoszM -!mulrzz -![_ *~ _]sumr_const -sumrB ler_sum // => y _.
-rewrite -(ler_add2r m%:Z) -PoszD subnK 1?ltnW // addrAC.
-by rewrite ler_subr_addr ler_add2l ler_subl_addr ler_paddr.
+rewrite -(lerD2r m%:Z) -PoszD subnK 1?ltnW // addrAC.
+by rewrite lerBrDr lerD2l lerBlDr ler_wpDr.
 Qed.
 
 Lemma source_drules_range : ~~ Pr58 nhub -> rs = [::].
@@ -401,7 +401,7 @@ Lemma dscore_cap2 (x : G) :
     arity x = nhub -> 0 < dscore x ->
   0 < dboundK + \sum_(y in cface x) dbound2 rt rs y.
 Proof.
-move=> nFx /lt_le_trans-> //; rewrite /dscore -dboundK_eq // ler_add2l.
+move=> nFx /lt_le_trans-> //; rewrite /dscore -dboundK_eq // lerD2l.
 do 2!rewrite (reindex_inj faceI) -(eq_bigl _ _ (fun y => cface1r y x)) /=.
 by apply: ler_sum => y xFy; rewrite dbound2_leq // -(arity_cface xFy).
 Qed.