diff --git a/complete_dioid.v b/complete_dioid.v
index f7ad264..c2dbd9e 100644
--- a/complete_dioid.v
+++ b/complete_dioid.v
@@ -462,7 +462,7 @@ HB.factory Record CompleteLattice_isComCompleteDioid d D
   addA : associative add;
   addC : commutative add;
   add0d : left_id zero add;
-  adddd : idempotent add;
+  adddd : idempotent_op add;
   mulA : associative mul;
   mulC : commutative mul;
   mul1d : left_id one mul;
diff --git a/complete_lattice.v b/complete_lattice.v
index e0d8a6b..da79d18 100644
--- a/complete_lattice.v
+++ b/complete_lattice.v
@@ -43,6 +43,8 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Import Order.Theory.
+(* remove below line when requireing mathcomp >= 2.4.0 *)
+Local Notation le_val := Order.le_val.
 
 Local Open Scope classical_set_scope.
 Local Open Scope order_scope.
@@ -707,9 +709,9 @@ Let set_meetU (B : set U) := inU (opredSM B).
 Lemma set_meetU_is_glb : set_f_is_glb set_meetU.
 Proof.
 move=> B; split.
-- by move=> x Bx; rewrite leEsub SubK set_meet_lb//; exists x.
-- move=> x ubx; rewrite leEsub SubK set_meet_ge_lb// => _ [y By <-].
-  by rewrite -leEsub ubx.
+- by move=> x Bx; rewrite -le_val SubK set_meet_lb//; exists x.
+- move=> x ubx; rewrite -le_val SubK set_meet_ge_lb// => _ [y By <-].
+  by rewrite le_val ubx.
 Qed.
 
 HB.instance Definition _ := POrder_isMeetCompleteLattice.Build d' U
@@ -717,14 +719,17 @@ HB.instance Definition _ := POrder_isMeetCompleteLattice.Build d' U
 
 Lemma val1 : (val : U -> T) \top = \top.
 Proof. by rewrite SubK image_set0 set_meet0. Qed.
+#[warning="-HB.no-new-instance"]
 HB.instance Definition _ := Order.isTSubLattice.Build d T S d' U val1.
 
 Lemma valI : Order.meet_morphism (val : U -> T).
 Proof. by move=> x y; rewrite SubK !image_setU !image_set1 set_meet2. Qed.
+#[warning="-HB.no-new-instance"]
 HB.instance Definition _ := Order.isMeetSubLattice.Build d T S d' U valI.
 
 Lemma valSM : set_meet_morphism (val : U -> T).
 Proof. by move=> B; rewrite SubK. Qed.
+#[warning="-HB.no-new-instance"]
 HB.instance Definition _ := isMeetSubCompleteLattice.Build d T S d' U valSM.
 
 HB.end.
@@ -759,9 +764,9 @@ Let set_joinU (B : set U) := inU (opredSJ B).
 Lemma set_joinU_is_lub : set_f_is_lub set_joinU.
 Proof.
 move=> B; split.
-- by move=> x Bx; rewrite leEsub SubK set_join_ub//; exists x.
-- move=> x ubx; rewrite leEsub SubK set_join_le_ub// => _ [y By <-].
-  by rewrite -leEsub ubx.
+- by move=> x Bx; rewrite -le_val SubK set_join_ub//; exists x.
+- move=> x ubx; rewrite -le_val SubK set_join_le_ub// => _ [y By <-].
+  by rewrite le_val ubx.
 Qed.
 
 HB.instance Definition _ := POrder_isJoinCompleteLattice.Build d' U
@@ -769,6 +774,7 @@ HB.instance Definition _ := POrder_isJoinCompleteLattice.Build d' U
 
 Lemma val0 : (val : U -> T) \bot = \bot.
 Proof. by rewrite SubK image_set0 set_join0. Qed.
+#[warning="-HB.no-new-instance"]
 HB.instance Definition _ := Order.isBSubLattice.Build d T S d' U val0.
 
 Lemma valU : Order.join_morphism (val : U -> T).
@@ -816,17 +822,17 @@ Let set_joinU (B : set U) := inU (opredSJ B).
 Lemma set_meetU_is_glb : set_f_is_glb set_meetU.
 Proof.
 move=> B; split.
-- by move=> x Bx; rewrite leEsub SubK set_meet_lb//; exists x.
-- move=> x lbx; rewrite leEsub SubK set_meet_ge_lb// => _ [y By <-].
-  by rewrite -leEsub lbx.
+- by move=> x Bx; rewrite -le_val SubK set_meet_lb//; exists x.
+- move=> x lbx; rewrite -le_val SubK set_meet_ge_lb// => _ [y By <-].
+  by rewrite le_val lbx.
 Qed.
 
 Lemma set_joinU_is_lub : set_f_is_lub set_joinU.
 Proof.
 move=> B; split.
-- by move=> x Bx; rewrite leEsub SubK set_join_ub//; exists x.
-- move=> x ubx; rewrite leEsub SubK set_join_le_ub// => _ [y By <-].
-  by rewrite -leEsub ubx.
+- by move=> x Bx; rewrite -le_val SubK set_join_ub//; exists x.
+- move=> x ubx; rewrite -le_val SubK set_join_le_ub// => _ [y By <-].
+  by rewrite le_val ubx.
 Qed.
 
 HB.instance Definition _ := POrder_isCompleteLattice.Build d' U
@@ -834,6 +840,7 @@ HB.instance Definition _ := POrder_isCompleteLattice.Build d' U
 
 Lemma val0 : (val : U -> T) \bot = \bot.
 Proof. by rewrite SubK image_set0 set_join0. Qed.
+#[warning="-HB.no-new-instance"]
 HB.instance Definition _ := Order.isBSubLattice.Build d T S d' U val0.
 
 Lemma val1 : (val : U -> T) \top = \top.
diff --git a/dioid.v b/dioid.v
index 03d404a..b129e01 100644
--- a/dioid.v
+++ b/dioid.v
@@ -73,7 +73,7 @@ Import Order.Theory GRing.Theory.
 
 HB.mixin Record SemiRing_POrder_isDioid d D
     of GRing.SemiRing D & Order.POrder d D := {
-  adddd : @idempotent D +%R;
+  adddd : @idempotent_op D +%R;
   le_def : forall (a b : D), (a <= b) = (a + b == b);
 }.
 
@@ -105,7 +105,7 @@ HB.factory Record POrder_isDioid d D of Order.POrder d D := {
   addA : associative add;
   addC : commutative add;
   add0d : left_id zero add;
-  adddd : idempotent add;
+  adddd : idempotent_op add;
   mulA : associative mul;
   mul1d : left_id one mul;
   muld1 : right_id one mul;
@@ -124,7 +124,7 @@ HB.instance Definition _ := SemiRing_POrder_isDioid.Build d D adddd le_def.
 HB.end.
 
 HB.factory Record SemiRing_isDioid (d : Order.disp_t) D of GRing.SemiRing D := {
-  adddd : @idempotent D +%R;
+  adddd : @idempotent_op D +%R;
 }.
 
 HB.builders Context d D of SemiRing_isDioid d D.
@@ -168,7 +168,7 @@ HB.factory Record Choice_isDioid (d : Order.disp_t) D of Choice D := {
   addA : associative add;
   addC : commutative add;
   add0d : left_id zero add;
-  adddd : idempotent add;
+  adddd : idempotent_op add;
   mulA : associative mul;
   mul1d : left_id one mul;
   muld1 : right_id one mul;
@@ -241,7 +241,7 @@ HB.factory Record POrder_isComDioid d D of Order.POrder d D := {
   addA : associative add;
   addC : commutative add;
   add0d : left_id zero add;
-  adddd : idempotent add;
+  adddd : idempotent_op add;
   mulA : associative mul;
   mulC : commutative mul;
   mul1d : left_id one mul;
@@ -277,7 +277,7 @@ HB.factory Record Choice_isComDioid (d : Order.disp_t) D of Choice D := {
   addA : associative add;
   addC : commutative add;
   add0d : left_id zero add;
-  adddd : idempotent add;
+  adddd : idempotent_op add;
   mulA : associative mul;
   mulC : commutative mul;
   mul1d : left_id one mul;
@@ -328,10 +328,10 @@ HB.factory Record SubSemiRing_SubPOrder_isSubDioid d (D : dioidType d) S d' U
     of GRing.SubSemiRing D S U & @Order.SubPOrder d D S d' U := {}.
 
 HB.builders Context d D S d' U of SubSemiRing_SubPOrder_isSubDioid d D S d' U.
-Lemma adddd : @idempotent U +%R.
+Lemma adddd : @idempotent_op U +%R.
 Proof. by move=> x; apply: val_inj; rewrite raddfD adddd. Qed.
 Lemma le_def (a b : U) : (a <= b) = (a + b == b).
-Proof. by rewrite leEsub le_def -rmorphD /= (inj_eq val_inj). Qed.
+Proof. by rewrite -Order.le_val le_def -rmorphD /= (inj_eq val_inj). Qed.
 HB.instance Definition _ := SemiRing_POrder_isDioid.Build d' U adddd le_def.
 HB.end.