diff --git a/RminStruct.v b/RminStruct.v
index a735af17937d6496c77411184071b774d878ff93..ec425258dc3f00320979b498115e386b282c658f 100644
--- a/RminStruct.v
+++ b/RminStruct.v
@@ -474,10 +474,10 @@ Definition Fplus_dioidE :=
 
 Lemma Fplus_divE (f g : Fplus) :
   ((f : Fplusd) / g)%D
-  = fun t => Order.max 0%dE
-      (ereal_sup [set (if g u == +oo then -oo
-                       else f (t%:nngnum + u%:nngnum)%:nng%R - g u)%dE
-                 | u in setT]) :> F.
+  = (fun t => Order.max 0%dE
+       (ereal_sup [set (if g u == +oo then -oo
+                        else f (t%:nngnum + u%:nngnum)%:nng%R - g u)%dE
+                  | u in setT])) :> F.
 Proof.
 apply/le_anti/andP; split; last first.
 { apply/lefP => t.
diff --git a/analysis_complements.v b/analysis_complements.v
index 3083b4832919ebf0a0cfc6713ece6609e263d6a1..35e113536d50c01e66b36a19d041b1c4019ca301 100644
--- a/analysis_complements.v
+++ b/analysis_complements.v
@@ -1,7 +1,8 @@
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrbool ssrfun order eqtype order seq.
 From mathcomp Require Import choice bigop ssrint intdiv ssralg ssrnum rat.
-From mathcomp.analysis Require Import constructive_ereal reals.
+From mathcomp Require Import archimedean.
+From mathcomp Require Import mathcomp_extra constructive_ereal reals.
 From mathcomp Require Import boolp classical_sets ereal signed.
 
 Set Implicit Arguments.
@@ -38,7 +39,7 @@ apply/(iffP idP).
   case: x y => [x||] [y||] //; last by move=> _ ? _; apply: leNye.
   by move=> xley e ?; rewrite (le_trans xley)// -dEFinD lee_fin ler_addl ltW.
 case: x y => [x||] [y||] // xleye.
-- by rewrite lee_fin; apply/mathcomp_extra.ler_addgt0Pr/xleye.
+- by rewrite lee_fin; apply/ler_addgt0Pr/xleye.
 - exact: leey.
 - exact: (le_trans (xleye 1%R _)).
 - by case: (xleye 1%R lte01).
@@ -170,18 +171,20 @@ Section Ceil.
 
 Context {R : realType}.
 
-Lemma ceilDz (x : R) (n : int) : ceil (x + n%:~R) = ceil x + n%:~R.
+Lemma ceilDz (x : R) (n : int) : Num.ceil (x + n%:~R) = Num.ceil x + n%:~R.
 Proof.
 apply/le_anti/andP; split.
   by rewrite -ceil_ge_int rmorphD/= intz ler_add2r ceil_ge.
 rewrite -ler_subr_addr -ceil_ge_int rmorphD/= intz !rmorphN/=.
-by rewrite -opprD -ler_oppr -ler_subr_addr opprD floor_le.
+by rewrite -opprD -ler_oppr -ler_subr_addr opprD reals.floor_le.
 Qed.
 
-Lemma gt_pred_ceil (x : R) : (ceil x)%:~R - 1 < x.
-Proof. by rewrite /ceil rmorphN -opprD ltr_oppl lt_succ_floor. Qed.
+Lemma gt_pred_ceil (x : R) : (Num.ceil x)%:~R - 1 < x.
+Proof.
+by rewrite /Num.ceil rmorphN/= -opprD ltr_oppl intrD1 lt_succ_floor ?num_real.
+Qed.
 
-Lemma ceilP (x : R) (n : int) : (n%:~R - 1 < x <= n%:~R) = (ceil x == n).
+Lemma ceilP (x : R) (n : int) : (n%:~R - 1 < x <= n%:~R) = (Num.ceil x == n).
 Proof.
 apply/idP/idP; last by move=> /eqP<-; rewrite ceil_ge gt_pred_ceil.
 move=> /andP[nltx xleSn]; apply/eqP/le_anti.
diff --git a/minerve/UPP.v b/minerve/UPP.v
index 3de1eabb51c1686704ae793eb40c2a71863c81b4..7fcedbe52e1275b8e88f3b175f3b4a6bd9f6ad83 100644
--- a/minerve/UPP.v
+++ b/minerve/UPP.v
@@ -1,8 +1,9 @@
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrbool ssrfun fintype ssrnat bigop.
 From mathcomp Require Import seq finfun path eqtype tuple choice order.
-From mathcomp Require Import ssralg ssrnum ssrint rat intdiv.
-From mathcomp Require Import boolp classical_sets signed reals ereal.
+From mathcomp Require Import ssralg ssrnum ssrint rat intdiv archimedean.
+From mathcomp Require Import mathcomp_extra boolp classical_sets signed reals.
+From mathcomp Require Import ereal.
 From NCCoq Require Import analysis_complements RminStruct.
 Require Import NCCoq.usual_functions.
 Require Import ratdiv.
@@ -42,7 +43,7 @@ Proof. by case: f. Qed.
 Definition F_UPP_of_F_def (f : F) (T d c : rat) : F :=
   fun (t : {nonneg R}) =>
     if t%:num <= ratr (T + d) then f t else
-      let n := (ceil ((t%:num - ratr T) / ratr d) - 1)%:~R in
+      let n := (Num.ceil ((t%:num - ratr T) / ratr d) - 1)%:~R in
       let t' := insubd 0%:nng (t%:num - ratr (n * d)) in
       f t' + (ratr (n * c))%:E.
 
@@ -148,16 +149,16 @@ Lemma F_UPP_min_aux (t : R) (T : {nonneg rat}) (d : {posnum rat}) :
     ratr T%:nngnum < t - ratr (k%:R * d%:num) <= ratr (T%:nngnum + d%:num).
 Proof.
 move=> Ht.
-pose zk := ceil ((t - ratr T%:nngnum) / ratr d%:num) - 1.
+pose zk := Num.ceil ((t - ratr T%:nngnum) / ratr d%:num) - 1.
 exists (absz zk).
 rewrite rmorphD rmorphM /= ltr_subr_addr ler_subl_addr -addrA.
 rewrite -ltr_subr_addl -ler_subl_addl.
 rewrite -{2}(mul1r (ratr d%:num)) -mulrDl (addrC 1).
 rewrite -ltr_pdivl_mulr ?ltr0q// -ler_pdivr_mulr ?ltr0q//.
 rewrite -[?[a]%:R]/((Posz ?[a])%:~R) gez0_abs; last first.
-{ rewrite subr_ge0 -gtz0_ge1 -ceil_lt_int.
+{ rewrite subr_ge0 -gtz0_ge1 -ceil_gt_int.
   by apply: divr_gt0; rewrite // subr_gt0. }
-rewrite ratr_int rmorphB/= subrK /ceil.
+rewrite ratr_int rmorphB/= subrK /Num.ceil.
 rewrite rmorphN/= -opprD ltr_oppl ler_oppr andbC -RfloorE.
 apply: mem_rg1_Rfloor.
 Qed.
diff --git a/static_priority.v b/static_priority.v
index c3e8a5f69c85ce26adc7ec440861eee55db5294a..120c1005715dca6b254dee9664b251519512f49e 100644
--- a/static_priority.v
+++ b/static_priority.v
@@ -212,7 +212,7 @@ have Di_uv u : u \in `]p, v] ->
   have {}D_beta_le_D :
     (D_hp_i u + D i u + beta (insubd 0%:nng (v%:num - u%:num))%R
      <= D_hp_i v + D i v)%dE.
-  { rewrite -(@lee_dadd2lE _ (D_lp_i v)); [|by rewrite -fin_flow_cc_sumE].
+  { rewrite -(@lee_dD2lE _ (D_lp_i v)); [|by rewrite -fin_flow_cc_sumE].
     rewrite !(daddeC (D_lp_i v)) daddeAC.
     have D_lp_i_uv : D_lp_i u = D_lp_i v.
     { rewrite !flow_cc_sumE.