diff --git a/theories/Crypt/package/pkg_advantage.v b/theories/Crypt/package/pkg_advantage.v
index db4a6ec4..680378c8 100644
--- a/theories/Crypt/package/pkg_advantage.v
+++ b/theories/Crypt/package/pkg_advantage.v
@@ -6,7 +6,7 @@ From SSProve.Relational Require Import OrderEnrichedCategory
   OrderEnrichedRelativeMonadExamples.
 Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format".
 From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype
-  choice reals distr seq all_algebra fintype realsum.
+  choice order reals distr seq all_algebra fintype realsum.
 Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format".
 From extructures Require Import ord fset fmap.
 From SSProve.Crypt Require Import Prelude Axioms ChoiceAsOrd SubDistr
@@ -207,7 +207,7 @@ Proof.
   intros P l Q A.
   induction l as [| R l ih] in P, Q |- *.
   - simpl. auto.
-  - simpl. eapply order.Order.POrderTheory.le_trans.
+  - simpl. eapply Order.POrderTheory.le_trans.
     + eapply Advantage_triangle.
     + eapply lerD.
       * auto.
diff --git a/theories/Crypt/package/pkg_rhl.v b/theories/Crypt/package/pkg_rhl.v
index 6f1c7ed9..873e5e5c 100644
--- a/theories/Crypt/package/pkg_rhl.v
+++ b/theories/Crypt/package/pkg_rhl.v
@@ -9,7 +9,7 @@ From SSProve.Relational Require Import OrderEnrichedCategory
   OrderEnrichedRelativeMonadExamples.
 Set Warnings "-ambiguous-paths,-notation-overridden,-notation-incompatible-format".
 From mathcomp Require Import ssrnat ssreflect ssrfun ssrbool ssrnum eqtype
-  choice reals distr seq all_algebra fintype realsum.
+  choice order reals distr seq all_algebra fintype realsum.
 Set Warnings "ambiguous-paths,notation-overridden,notation-incompatible-format".
 From extructures Require Import ord fset fmap.
 From SSProve.Mon Require Import SPropBase.
@@ -98,7 +98,7 @@ Proof.
     { destruct ((get_heap s₁ ℓ, s₁, (get_heap s₂ ℓ, s₂)) == (b₁, s₃, (b₂, s₄))) eqn:e.
       - move: e => /eqP e. assumption.
       - rewrite e in hd. cbn in hd.
-        rewrite order.Order.POrderTheory.ltxx in hd. discriminate.
+        rewrite Order.POrderTheory.ltxx in hd. discriminate.
     }
     inversion e. subst. intuition auto.
 Qed.
@@ -130,7 +130,7 @@ Proof.
     { destruct ((tt, set_heap s1 l v, (tt, set_heap s2 l v)) == (b1, s3, (b2, s4))) eqn:Heqd.
       - move: Heqd. move /eqP => Heqd. assumption.
       - rewrite Heqd in Hd. simpl in Hd.
-        rewrite order.Order.POrderTheory.ltxx in Hd. discriminate.
+        rewrite Order.POrderTheory.ltxx in Hd. discriminate.
     }
     inversion Heqs.
     intuition eauto.
@@ -178,21 +178,21 @@ Proof.
   assert (realsum.psum f ≠ 0) as Hneq.
   { intros Hgt.
     rewrite Hgt in H.
-    rewrite order.Order.POrderTheory.ltxx in H.
+    rewrite Order.POrderTheory.ltxx in H.
     auto. }
   destruct (realsum.neq0_psum (R:=R) Hneq) as [x Hx].
   exists x. specialize (Hpos x).
-  rewrite order.Order.POrderTheory.le_eqVlt in Hpos.
+  rewrite Order.POrderTheory.le_eqVlt in Hpos.
   move: Hpos. move /orP => [H1 | H2].
   - move: H1. move /eqP => H1. rewrite -H1.
-    rewrite order.Order.POrderTheory.ltxx. auto.
+    rewrite Order.POrderTheory.ltxx. auto.
   - assumption.
 Qed.
 
 Lemma pmulr_me (x y : R) : 0 <= y -> (0 < y * x) -> (0 < x).
 Proof.
   rewrite le0r => /orP[/eqP->|].
-  - by rewrite GRing.mul0r order.Order.POrderTheory.ltxx.
+  - by rewrite GRing.mul0r Order.POrderTheory.ltxx.
   - intros. by rewrite -(pmulr_rgt0 x b).
 Qed.
 
@@ -201,7 +201,7 @@ Lemma ge0_eq {R : realType} {A : eqType} {x y : A} (H : 0 < ((x == y)%:R) :> R)
 Proof.
   destruct (x == y) eqn:Heq.
   - move: Heq. by move /eqP.
-  - by rewrite order.Order.POrderTheory.ltxx in H.
+  - by rewrite Order.POrderTheory.ltxx in H.
 Qed.
 
 Lemma ne0_eq {R : ringType} {A : eqType} {x y : A} (H : ((x == y)%:R) ≠ (0 : R)) :
@@ -1265,7 +1265,7 @@ Proof.
     end.
     2:{
       rewrite e in hh. simpl in hh.
-      rewrite order.Order.POrderTheory.ltxx in hh. discriminate.
+      rewrite Order.POrderTheory.ltxx in hh. discriminate.
     }
     move: e => /eqP e. inversion e.
     subst. assumption.
@@ -2569,7 +2569,7 @@ Proof.
       unfold SDistr_bind. rewrite dlet_null.
       reflexivity.
   - intros [? ?] [? ?]. rewrite dnullE.
-    rewrite order.Order.POrderTheory.ltxx. discriminate.
+    rewrite Order.POrderTheory.ltxx. discriminate.
 Qed.
 
 Lemma r_assert' :
@@ -2635,7 +2635,7 @@ Proof.
       unfold SDistr_bind. rewrite dlet_null.
       reflexivity.
   - intros [? ?] [? ?]. rewrite dnullE.
-    rewrite order.Order.POrderTheory.ltxx. discriminate.
+    rewrite Order.POrderTheory.ltxx. discriminate.
 Qed.
 
 Theorem r_assertD :
@@ -2690,7 +2690,7 @@ Proof.
         unfold SDistr_bind. rewrite dlet_null.
         reflexivity.
     + intros [? ?] [? ?]. rewrite dnullE.
-      rewrite order.Order.POrderTheory.ltxx. discriminate.
+      rewrite Order.POrderTheory.ltxx. discriminate.
 Qed.
 
 Lemma rswap_assertD_cmd_eq :
@@ -2762,7 +2762,7 @@ Proof.
         unfold SDistr_bind. rewrite dlet_null.
         reflexivity.
     + intros [? ?] [? ?]. rewrite dnullE.
-      rewrite order.Order.POrderTheory.ltxx. discriminate.
+      rewrite Order.POrderTheory.ltxx. discriminate.
 Qed.
 
 Lemma r_bind_assertD_sym :
@@ -2812,7 +2812,7 @@ Proof.
     end.
     2:{
       rewrite e in hh. simpl in hh.
-      rewrite order.Order.POrderTheory.ltxx in hh. discriminate.
+      rewrite Order.POrderTheory.ltxx in hh. discriminate.
     }
     move: e => /eqP e. inversion e.
     subst. reflexivity.
@@ -2885,7 +2885,7 @@ Proof.
     end.
     2:{
       rewrite e in hh. simpl in hh.
-      rewrite order.Order.POrderTheory.ltxx in hh. discriminate.
+      rewrite Order.POrderTheory.ltxx in hh. discriminate.
     }
     move: e => /eqP e. inversion e.
     subst.
@@ -2929,7 +2929,7 @@ Proof.
     end.
     2:{
       rewrite e in hh. simpl in hh.
-      rewrite order.Order.POrderTheory.ltxx in hh. discriminate.
+      rewrite Order.POrderTheory.ltxx in hh. discriminate.
     }
     move: e => /eqP e. noconf e.
     subst. f_equal.