diff --git a/complete_dioid.v b/complete_dioid.v
index c2dbd9e..6912d49 100644
--- a/complete_dioid.v
+++ b/complete_dioid.v
@@ -59,7 +59,7 @@ Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
 Reserved Notation "x ^+" (at level 2, format "x ^+").
-Reserved Notation "x ^*" (at level 2, format "x ^*").
+Reserved Notation "x ^*" (at level 1, left associativity, format "x ^*").
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
@@ -68,7 +68,7 @@ Local Open Scope dioid_scope.
 
 Import Order.Theory GRing.Theory.
 
-HB.mixin Record isCompleteDioid d D of Dioid d D & CompleteLattice d D := {
+HB.mixin Record isCompleteDioid d D & Dioid d D & CompleteLattice d D := {
   set_mulDl : forall (a : D) (B : set D),
       a * set_join B = set_join [set a * x | x in B];
   set_mulDr : forall (a : D) (B : set D),
@@ -253,7 +253,7 @@ suff Hyp : forall i, (a + 1) ^ i = set_add [set a ^ j | j in [set x | 'I_i.+1 x]
 elim=> [ | i IHi]; [by rewrite set_add1 !exp0|].
 rewrite expS mulrDl mul1r IHi set_mulDl.
 set B' := [set a ^ j | j in [set j | (1 <= j <= i)%N]].
-rewrite [X in set_join X](_ : _ = a ^ i.+1 |` B'); last first.
+rewrite [X in set_join X](_ : _ = a ^ i.+1 |` B').
 { rewrite predeqP => x; split.
   - move=> -[y [[j Hj] _ <-] <-].
     rewrite expS /= -!expS.
@@ -263,7 +263,7 @@ rewrite [X in set_join X](_ : _ = a ^ i.+1 |` B'); last first.
     move=> -[[//|j] /andP [Hj Hji] <-]; rewrite expS; exists (a ^ j) => //.
     by move: Hji => /ltnW; rewrite -ltnS => Hji; exists (Ordinal Hji). }
 rewrite -[set_join]/set_add set_addDl.
-rewrite (_ : image _ _ = (1%R |` B')); last first.
+rewrite (_ : image _ _ = (1%R |` B')).
 { rewrite predeqP => x; split.
   { move=> -[[[|j] Hj] _ <-]; [by left; rewrite exp0|].
     by right; exists (Ordinal Hj). }
@@ -286,7 +286,7 @@ Lemma kleene_sqr a : a^* * a^* = a^*.
 Proof.
 rewrite {1}/op_kleene set_mulDr.
 set B' := (a ^* |` (range (fun i => a ^ i.+1 * a ^*))).
-rewrite (_ : image _ _ = B'); last first.
+rewrite (_ : image _ _ = B').
 { rewrite predeqP => x; split.
   - by move=> -[_ [[|i] _ <-] <-]; [left; rewrite exp0 mul1r|right; exists i].
   - move=> [-> | [i _ <-]]; [by exists 1%R; [exists O|rewrite mul1r]|].
@@ -310,7 +310,7 @@ Qed.
 Lemma kleene_kleene a : (a ^*) ^* = a ^*.
 Proof.
 rewrite kleeneSr /op_plus.
-rewrite (_ : image _ _ = a ^* |` set0).
+rewrite (_ : image _ _ = a ^* |` set0); last first.
   by rewrite setU0 set_join1 kleeneSr addrA adddd.
 rewrite predeqP => x; split.
 - move=> [i _ <-]; left; exact: kleene_exp.
@@ -324,7 +324,7 @@ Theorem kleene_star_least a b : forall x, (x = a * x + b) -> a ^* * b <= x.
 Proof.
 move=> x Hx.
 rewrite set_mulDr.
-rewrite [X in set_join X](_ : _ = [set (a ^ i) * b | i in setT]); last first.
+rewrite [X in set_join X](_ : _ = [set (a ^ i) * b | i in setT]).
   rewrite predeqP => y; split.
   - by move=> [_ [i _ <-] <-]; exists i.
   - by move=> [i _ <-]; exists (a ^ i); [exists i|].
@@ -435,15 +435,15 @@ Notation "a / b" := (div a b) : dioid_scope.
 
 #[short(type="comCompleteDioidType")]
 HB.structure Definition ComCompleteDioid d :=
-  { D of GRing.ComSemiRing D & CompleteDioid d D }.
+  { D of GRing.ComNzSemiRing D & CompleteDioid d D }.
 
 HB.factory Record isComCompleteDioid d D
-    of ComDioid d D & CompleteLattice d D := {
+    & ComDioid d D & CompleteLattice d D := {
   set_mulDl : forall (a : D) (B : set D),
     a * set_join B = set_join [set a * x | x in B];
 }.
 
-HB.builders Context d D of isComCompleteDioid d D.
+HB.builders Context d D & isComCompleteDioid d D.
 Lemma set_mulDr a (B : set D) :
   set_join B * a = set_join [set x * a | x in B].
 Proof.
@@ -454,7 +454,7 @@ HB.instance Definition _ := isCompleteDioid.Build d D set_mulDl set_mulDr.
 HB.end.
 
 HB.factory Record CompleteLattice_isComCompleteDioid d D
-    of CompleteLattice d D := {
+    & CompleteLattice d D := {
   zero : D;
   add : D -> D -> D;
   one : D;
@@ -474,7 +474,7 @@ HB.factory Record CompleteLattice_isComCompleteDioid d D
     mul a (set_join B) = set_join [set mul a x | x in B];
 }.
 
-HB.builders Context d D of CompleteLattice_isComCompleteDioid d D.
+HB.builders Context d D & CompleteLattice_isComCompleteDioid d D.
 HB.instance Definition _ := POrder_isComDioid.Build d D
   addA addC add0d adddd mulA mulC mul1d mulDl mul0d oner_neq0 le_def.
 HB.instance Definition _ := isComCompleteDioid.Build d D set_mulDl.
@@ -552,10 +552,10 @@ HB.structure Definition SubCompleteDioid d (D : completeDioidType d) S d' :=
 
 HB.factory Record SubDioid_JoinSubCompleteLattice_isJoinSubCompleteDioid
     d (D : completeDioidType d) S d' U
-    of @SubDioid d D S d' U & @JoinSubCompleteLattice d D S d' U := {}.
+    & @SubDioid d D S d' U & @JoinSubCompleteLattice d D S d' U := {}.
 
 HB.builders Context d D S d' U
-  of SubDioid_JoinSubCompleteLattice_isJoinSubCompleteDioid d D S d' U.
+  & SubDioid_JoinSubCompleteLattice_isJoinSubCompleteDioid d D S d' U.
 Lemma set_mulDl (a : U) (B : set U) :
   a * set_join B = set_join [set a * x | x in B].
 Proof.
@@ -573,12 +573,12 @@ HB.end.
 
 HB.factory Record SubDioid_SubPOrder_isJoinSubCompleteDioid d
     (D : completeDioidType d) S d' U
-    of @SubDioid d D S d' U & @Order.SubPOrder d D S d' U := {
+    & @SubDioid d D S d' U & @Order.SubPOrder d D S d' U := {
   opredSJ_subproof : set_join_closed S;
 }.
 
 HB.builders Context d D S d' U
-  of SubDioid_SubPOrder_isJoinSubCompleteDioid d D S d' U.
+  & SubDioid_SubPOrder_isJoinSubCompleteDioid d D S d' U.
 HB.instance Definition _ := SubPOrder_isJoinSubCompleteLattice.Build d D S d' U
   opredSJ_subproof.
 HB.instance Definition _ :=
@@ -586,12 +586,12 @@ HB.instance Definition _ :=
 HB.end.
 
 HB.factory Record SubChoice_isJoinSubCompleteDioid d (D : completeDioidType d)
-    S (d' : Order.disp_t) U of SubChoice D S U := {
+    S (d' : Order.disp_t) U & SubChoice D S U := {
   semiring_closed_subproof : semiring_closed S;
   opredSJ_subproof : set_join_closed S;
 }.
 
-HB.builders Context d D S d' U of SubChoice_isJoinSubCompleteDioid d D S d' U.
+HB.builders Context d D S d' U & SubChoice_isJoinSubCompleteDioid d D S d' U.
 HB.instance Definition _ := SubChoice_isSubDioid.Build d D S d' U
   semiring_closed_subproof.
 HB.instance Definition _ :=
@@ -599,13 +599,13 @@ HB.instance Definition _ :=
 HB.end.
 
 HB.factory Record SubChoice_isJoinSubComCompleteDioid d
-    (D : comCompleteDioidType d) S (d' : Order.disp_t) U of SubChoice D S U := {
+    (D : comCompleteDioidType d) S (d' : Order.disp_t) U & SubChoice D S U := {
   semiring_closed_subproof : semiring_closed S;
   opredSJ_subproof : set_join_closed S;
 }.
 
 HB.builders Context d D S d' U
-  of SubChoice_isJoinSubComCompleteDioid d D S d' U.
+  & SubChoice_isJoinSubComCompleteDioid d D S d' U.
 HB.instance Definition _ := SubChoice_isJoinSubCompleteDioid.Build d D S d' U
   semiring_closed_subproof opredSJ_subproof.
 HB.instance Definition _ := GRing.SubSemiRing_isSubComSemiRing.Build D S U.
@@ -613,10 +613,10 @@ HB.end.
 
 HB.factory Record SubDioid_SubCompleteLattice_isSubCompleteDioid
     d (D : completeDioidType d) S d' U
-    of @SubDioid d D S d' U & @SubCompleteLattice d D S d' U := {}.
+    & @SubDioid d D S d' U & @SubCompleteLattice d D S d' U := {}.
 
 HB.builders Context d D S d' U
-  of SubDioid_SubCompleteLattice_isSubCompleteDioid d D S d' U.
+  & SubDioid_SubCompleteLattice_isSubCompleteDioid d D S d' U.
 Lemma set_mulDl (a : U) (B : set U) :
   a * set_join B = set_join [set a * x | x in B].
 Proof.
@@ -634,13 +634,13 @@ HB.end.
 
 HB.factory Record SubDioid_SubPOrder_isSubCompleteDioid d
     (D : completeDioidType d) S d' U
-    of @SubDioid d D S d' U & @Order.SubPOrder d D S d' U := {
+    & @SubDioid d D S d' U & @Order.SubPOrder d D S d' U := {
   opredSM_subproof : set_meet_closed S;
   opredSJ_subproof : set_join_closed S;
 }.
 
 HB.builders Context d D S d' U
-  of SubDioid_SubPOrder_isSubCompleteDioid d D S d' U.
+  & SubDioid_SubPOrder_isSubCompleteDioid d D S d' U.
 HB.instance Definition _ := SubPOrder_isSubCompleteLattice.Build d D S d' U
   opredSM_subproof opredSJ_subproof.
 HB.instance Definition _ :=
@@ -648,13 +648,13 @@ HB.instance Definition _ :=
 HB.end.
 
 HB.factory Record SubChoice_isSubCompleteDioid d (D : completeDioidType d) S
-    (d' : Order.disp_t) U of SubChoice D S U := {
+    (d' : Order.disp_t) U & SubChoice D S U := {
   semiring_closed_subproof : semiring_closed S;
   opredSM_subproof : set_meet_closed S;
   opredSJ_subproof : set_join_closed S;
 }.
 
-HB.builders Context d D S d' U of SubChoice_isSubCompleteDioid d D S d' U.
+HB.builders Context d D S d' U & SubChoice_isSubCompleteDioid d D S d' U.
 HB.instance Definition _ := SubChoice_isSubDioid.Build d D S d' U
   semiring_closed_subproof.
 HB.instance Definition _ :=
@@ -663,14 +663,14 @@ HB.instance Definition _ :=
 HB.end.
 
 HB.factory Record SubChoice_isSubComCompleteDioid d
-    (D : comCompleteDioidType d) S (d' : Order.disp_t) U of SubChoice D S U := {
+    (D : comCompleteDioidType d) S (d' : Order.disp_t) U & SubChoice D S U := {
   semiring_closed_subproof : semiring_closed S;
   opredSM_subproof : set_meet_closed S;
   opredSJ_subproof : set_join_closed S;
 }.
 
 HB.builders Context d D S d' U
-  of SubChoice_isSubComCompleteDioid d D S d' U.
+  & SubChoice_isSubComCompleteDioid d D S d' U.
 HB.instance Definition _ := SubChoice_isSubCompleteDioid.Build d D S d' U
   semiring_closed_subproof opredSM_subproof opredSJ_subproof.
 HB.instance Definition _ := GRing.SubSemiRing_isSubComSemiRing.Build D S U.
diff --git a/complete_lattice.v b/complete_lattice.v
index da79d18..f8dc808 100644
--- a/complete_lattice.v
+++ b/complete_lattice.v
@@ -65,7 +65,7 @@ Definition set_f_is_glb d (T : porderType d) (set_f : set T -> T) :=
 Definition set_f_is_lub d (T : porderType d) (set_f : set T -> T) :=
   forall S, ubound S (set_f S) /\ forall x, ubound S x -> set_f S <= x.
 
-HB.mixin Record isCompleteLattice d T of Order.POrder d T := {
+HB.mixin Record isCompleteLattice d T & Order.POrder d T := {
   set_meet : set T -> T;
   set_meet_is_glb : set_f_is_glb set_meet;
   set_join : set T -> T;
@@ -76,14 +76,14 @@ HB.mixin Record isCompleteLattice d T of Order.POrder d T := {
 HB.structure Definition CompleteLattice d :=
   { T of Order.TBLattice d T & isCompleteLattice d T }.
 
-HB.factory Record POrder_isCompleteLattice d T of Order.POrder d T := {
+HB.factory Record POrder_isCompleteLattice d T & Order.POrder d T := {
   set_meet : set T -> T;
   set_meet_is_glb : set_f_is_glb set_meet;
   set_join : set T -> T;
   set_join_is_lub : set_f_is_lub set_join;
 }.
 
-HB.builders Context d T of POrder_isCompleteLattice d T.
+HB.builders Context d T & POrder_isCompleteLattice d T.
 
 Lemma set_join_ub S : ubound S (set_join S).
 Proof. exact: (set_join_is_lub S).1. Qed.
@@ -231,12 +231,12 @@ HB.instance Definition _ := isCompleteLattice.Build d T
 
 HB.end.
 
-HB.factory Record POrder_isMeetCompleteLattice d T of Order.POrder d T := {
+HB.factory Record POrder_isMeetCompleteLattice d T & Order.POrder d T := {
   set_meet : set T -> T;
   set_meet_is_glb : set_f_is_glb set_meet;
 }.
 
-HB.builders Context d T of POrder_isMeetCompleteLattice d T.
+HB.builders Context d T & POrder_isMeetCompleteLattice d T.
 Definition set_join S := set_meet (ubound S).
 Lemma set_join_is_lub : set_f_is_lub set_join.
 Proof.
@@ -247,12 +247,12 @@ HB.instance Definition _ := POrder_isCompleteLattice.Build d T
   set_meet_is_glb set_join_is_lub.
 HB.end.
 
-HB.factory Record POrder_isJoinCompleteLattice d T of Order.POrder d T := {
+HB.factory Record POrder_isJoinCompleteLattice d T & Order.POrder d T := {
   set_join : set T -> T;
   set_join_is_lub : set_f_is_lub set_join;
 }.
 
-HB.builders Context d T of POrder_isJoinCompleteLattice d T.
+HB.builders Context d T & POrder_isJoinCompleteLattice d T.
 Definition set_meet S := set_join (lbound S).
 Lemma set_meet_is_glb : set_f_is_glb set_meet.
 Proof.
@@ -454,11 +454,11 @@ HB.structure Definition CompleteLatticeMorphism
 
 HB.factory Record isMeetCompleteLatticeMorphism d (L : completeLatticeType d)
     d' (L' : completeLatticeType d') (apply : L -> L')
-    of @Order.OrderMorphism d L d' L' apply := {
+    & @Order.OrderMorphism d L d' L' apply := {
   omorphSM : set_meet_morphism apply;
 }.
 
-HB.builders Context d L d' L' f of isMeetCompleteLatticeMorphism d L d' L' f.
+HB.builders Context d L d' L' f & isMeetCompleteLatticeMorphism d L d' L' f.
 Lemma omorphI : Order.meet_morphism f.
 Proof. by move=> x y; rewrite -!set_meet2 omorphSM !image_setU !image_set1. Qed.
 HB.instance Definition _ := Order.isMeetLatticeMorphism.Build d L d' L' f
@@ -471,11 +471,11 @@ HB.end.
 
 HB.factory Record isJoinCompleteLatticeMorphism d (L : completeLatticeType d)
     d' (L' : completeLatticeType d') (apply : L -> L')
-    of @Order.OrderMorphism d L d' L' apply := {
+    & @Order.OrderMorphism d L d' L' apply := {
   omorphSJ : set_join_morphism apply;
 }.
 
-HB.builders Context d L d' L' f of isJoinCompleteLatticeMorphism d L d' L' f.
+HB.builders Context d L d' L' f & isJoinCompleteLatticeMorphism d L d' L' f.
 Lemma omorphU : Order.join_morphism f.
 Proof. by move=> x y; rewrite -!set_join2 omorphSJ !image_setU !image_set1. Qed.
 HB.instance Definition _ := Order.isJoinLatticeMorphism.Build d L d' L' f
@@ -488,12 +488,12 @@ HB.end.
 
 HB.factory Record isCompleteLatticeMorphism d (L : completeLatticeType d)
     d' (L' : completeLatticeType d') (apply : L -> L')
-    of @Order.OrderMorphism d L d' L' apply := {
+    & @Order.OrderMorphism d L d' L' apply := {
   omorphSM : set_meet_morphism apply;
   omorphSJ : set_join_morphism apply;
 }.
 
-HB.builders Context d L d' L' f of isCompleteLatticeMorphism d L d' L' f.
+HB.builders Context d L d' L' f & isCompleteLatticeMorphism d L d' L' f.
 HB.instance Definition _ := isMeetCompleteLatticeMorphism.Build d L d' L' f
   omorphSM.
 HB.instance Definition _ := isJoinCompleteLatticeMorphism.Build d L d' L' f
@@ -611,7 +611,7 @@ HB.factory Record isMeetCompleteLatticeClosed d (T : completeLatticeType d)
   opredSM : set_meet_closed S;
 }.
 
-HB.builders Context d T S of isMeetCompleteLatticeClosed d T S.
+HB.builders Context d T S & isMeetCompleteLatticeClosed d T S.
 Lemma opred1 : \top \in S. Proof. by rewrite -set_meet0 opredSM. Qed.
 HB.instance Definition _ := Order.isTLatticeClosed.Build d T S opred1.
 Lemma opredI : meet_closed S.
@@ -625,7 +625,7 @@ HB.factory Record isJoinCompleteLatticeClosed d (T : completeLatticeType d)
   opredSJ : set_join_closed S;
 }.
 
-HB.builders Context d T S of isJoinCompleteLatticeClosed d T S.
+HB.builders Context d T S & isJoinCompleteLatticeClosed d T S.
 Lemma opred0 : \bot \in S. Proof. by rewrite -set_join0 opredSJ. Qed.
 HB.instance Definition _ := Order.isBLatticeClosed.Build d T S opred0.
 Lemma opredU : join_closed S.
@@ -640,7 +640,7 @@ HB.factory Record isCompleteLatticeClosed d (T : completeLatticeType d)
   opredSJ : set_join_closed S;
 }.
 
-HB.builders Context d T S of isCompleteLatticeClosed d T S.
+HB.builders Context d T S & isCompleteLatticeClosed d T S.
 HB.instance Definition _ := isMeetCompleteLatticeClosed.Build d T S opredSM.
 HB.instance Definition _ := isJoinCompleteLatticeClosed.Build d T S opredSJ.
 HB.end.
@@ -649,12 +649,12 @@ Arguments opredSM {d T} _.
 Arguments opredSJ {d T} _.
 
 HB.mixin Record isMeetSubCompleteLattice d (T : completeLatticeType d)
-    (S : pred T) d' U of SubType T S U & CompleteLattice d' U := {
+    (S : pred T) d' U & SubType T S U & CompleteLattice d' U := {
   valSM_subproof : set_meet_morphism (val : U -> T);
 }.
 
 HB.mixin Record isJoinSubCompleteLattice d (T : completeLatticeType d)
-    (S : pred T) d' U of SubType T S U & CompleteLattice d' U := {
+    (S : pred T) d' U & SubType T S U & CompleteLattice d' U := {
   valSJ_subproof : set_join_morphism (val : U -> T);
 }.
 
@@ -691,11 +691,11 @@ HB.instance Definition _ (d : Order.disp_t) (T : completeLatticeType d)
   isJoinCompleteLatticeMorphism.Build d' U d T val valSJ_subproof.
 
 HB.factory Record SubPOrder_isMeetSubCompleteLattice d
-    (T : completeLatticeType d) S d' U of @Order.SubPOrder d T S d' U := {
+    (T : completeLatticeType d) S d' U & @Order.SubPOrder d T S d' U := {
   opredSM_subproof : set_meet_closed S;
 }.
 
-HB.builders Context d T S d' U of SubPOrder_isMeetSubCompleteLattice d T S d' U.
+HB.builders Context d T S d' U & SubPOrder_isMeetSubCompleteLattice d T S d' U.
 
 HB.instance Definition _ := isMeetCompleteLatticeClosed.Build d T S
   opredSM_subproof.
@@ -735,22 +735,22 @@ HB.instance Definition _ := isMeetSubCompleteLattice.Build d T S d' U valSM.
 HB.end.
 
 HB.factory Record SubChoice_isMeetSubCompleteLattice d
-    (T : completeLatticeType d) S (d' : Order.disp_t) U of SubChoice T S U := {
+    (T : completeLatticeType d) S (d' : Order.disp_t) U & SubChoice T S U := {
   opredSM_subproof : set_meet_closed S;
 }.
 
-HB.builders Context d T S d' U of SubChoice_isMeetSubCompleteLattice d T S d' U.
+HB.builders Context d T S d' U & SubChoice_isMeetSubCompleteLattice d T S d' U.
 HB.instance Definition _ := Order.SubChoice_isSubPOrder.Build d T S d' U.
 HB.instance Definition _ := SubPOrder_isMeetSubCompleteLattice.Build d T S d' U
   opredSM_subproof.
 HB.end.
 
 HB.factory Record SubPOrder_isJoinSubCompleteLattice d
-    (T : completeLatticeType d) S d' U of @Order.SubPOrder d T S d' U := {
+    (T : completeLatticeType d) S d' U & @Order.SubPOrder d T S d' U := {
   opredSJ_subproof : set_join_closed S;
 }.
 
-HB.builders Context d T S d' U of SubPOrder_isJoinSubCompleteLattice d T S d' U.
+HB.builders Context d T S d' U & SubPOrder_isJoinSubCompleteLattice d T S d' U.
 
 HB.instance Definition _ := isJoinCompleteLatticeClosed.Build d T S
   opredSJ_subproof.
@@ -788,23 +788,23 @@ HB.instance Definition _ := isJoinSubCompleteLattice.Build d T S d' U valSJ.
 HB.end.
 
 HB.factory Record SubChoice_isJoinSubCompleteLattice d
-    (T : completeLatticeType d) S (d' : Order.disp_t) U of SubChoice T S U := {
+    (T : completeLatticeType d) S (d' : Order.disp_t) U & SubChoice T S U := {
   opredSJ_subproof : set_join_closed S;
 }.
 
-HB.builders Context d T S d' U of SubChoice_isJoinSubCompleteLattice d T S d' U.
+HB.builders Context d T S d' U & SubChoice_isJoinSubCompleteLattice d T S d' U.
 HB.instance Definition _ := Order.SubChoice_isSubPOrder.Build d T S d' U.
 HB.instance Definition _ := SubPOrder_isJoinSubCompleteLattice.Build d T S d' U
   opredSJ_subproof.
 HB.end.
 
 HB.factory Record SubPOrder_isSubCompleteLattice d
-    (T : completeLatticeType d) S d' U of @Order.SubPOrder d T S d' U := {
+    (T : completeLatticeType d) S d' U & @Order.SubPOrder d T S d' U := {
   opredSM_subproof : set_meet_closed S;
   opredSJ_subproof : set_join_closed S;
 }.
 
-HB.builders Context d T S d' U of SubPOrder_isSubCompleteLattice d T S d' U.
+HB.builders Context d T S d' U & SubPOrder_isSubCompleteLattice d T S d' U.
 
 HB.instance Definition _ := isCompleteLatticeClosed.Build d T S
   opredSM_subproof opredSJ_subproof.
@@ -866,12 +866,12 @@ HB.instance Definition _ := isJoinSubCompleteLattice.Build d T S d' U valSJ.
 HB.end.
 
 HB.factory Record SubChoice_isSubCompleteLattice d
-    (T : completeLatticeType d) S (d' : Order.disp_t) U of SubChoice T S U := {
+    (T : completeLatticeType d) S (d' : Order.disp_t) U & SubChoice T S U := {
   opredSM_subproof : set_meet_closed S;
   opredSJ_subproof : set_join_closed S;
 }.
 
-HB.builders Context d T S d' U of SubChoice_isSubCompleteLattice d T S d' U.
+HB.builders Context d T S d' U & SubChoice_isSubCompleteLattice d T S d' U.
 HB.instance Definition _ := Order.SubChoice_isSubPOrder.Build d T S d' U.
 HB.instance Definition _ := SubPOrder_isSubCompleteLattice.Build d T S d' U
   opredSM_subproof opredSJ_subproof.
diff --git a/coq-mathcomp-dioid.opam b/coq-mathcomp-dioid.opam
index 499a15d..186053b 100644
--- a/coq-mathcomp-dioid.opam
+++ b/coq-mathcomp-dioid.opam
@@ -15,9 +15,12 @@ build: [
 install: [make "install"]
 
 depends: [
-  "coq" { >= "8.20" & < "8.21~" }
-  "coq-mathcomp-algebra" { >= "2.3" & < "2.4~" }
-  "coq-mathcomp-classical" { >= "1.8" & < "1.9~" }
+  # Only tested against Rocq 9.4+alpha and the mathcomp/analysis dev
+  # branches: this revision uses the MathComp 2.6 Nz* ring hierarchy and the
+  # `&` spelling of HB's factory clause.
+  "coq" { >= "9.4~" }
+  "coq-mathcomp-algebra" { >= "2.6" }
+  "coq-mathcomp-classical" { >= "1.8" }
   "coq-hierarchy-builder" { >= "1.8.0" }
 ]
 synopsis: "Dioid"
diff --git a/dioid.v b/dioid.v
index b129e01..cfa3285 100644
--- a/dioid.v
+++ b/dioid.v
@@ -72,14 +72,14 @@ Local Open Scope dioid_scope.
 Import Order.Theory GRing.Theory.
 
 HB.mixin Record SemiRing_POrder_isDioid d D
-    of GRing.SemiRing D & Order.POrder d D := {
+    & GRing.NzSemiRing D & Order.POrder d D := {
   adddd : @idempotent_op D +%R;
   le_def : forall (a b : D), (a <= b) = (a + b == b);
 }.
 
 #[short(type="dioidType")]
 HB.structure Definition Dioid d :=
-  { D of SemiRing_POrder_isDioid d D & GRing.SemiRing D & Order.POrder d D }.
+  { D of SemiRing_POrder_isDioid d D & GRing.NzSemiRing D & Order.POrder d D }.
 
 #[short(type="dioidLatticeType")]
 HB.structure Definition DioidLattice d :=
@@ -97,7 +97,7 @@ HB.structure Definition DioidTLattice d :=
 HB.structure Definition DioidTBLattice d :=
   { D of Dioid d D & Order.TBLattice d D }.
 
-HB.factory Record POrder_isDioid d D of Order.POrder d D := {
+HB.factory Record POrder_isDioid d D & Order.POrder d D := {
   zero : D;
   add : D -> D -> D;
   one : D;
@@ -117,17 +117,17 @@ HB.factory Record POrder_isDioid d D of Order.POrder d D := {
   le_def : forall (a b : D), (a <= b) = (add a b == b);
 }.
 
-HB.builders Context d D of POrder_isDioid d D.
-HB.instance Definition _ := GRing.isSemiRing.Build D addA addC add0d
+HB.builders Context d D & POrder_isDioid d D.
+HB.instance Definition _ := GRing.isNzSemiRing.Build D addA addC add0d
   mulA mul1d muld1 mulDl mulDr mul0d muld0 oner_neq0.
 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 := {
+HB.factory Record SemiRing_isDioid (d : Order.disp_t) D & GRing.NzSemiRing D := {
   adddd : @idempotent_op D +%R;
 }.
 
-HB.builders Context d D of SemiRing_isDioid d D.
+HB.builders Context d D & SemiRing_isDioid d D.
 
 Definition le_dioid (a b : D) := a + b == b.
 
@@ -160,7 +160,7 @@ HB.instance Definition _ := SemiRing_POrder_isDioid.Build d D adddd le_def.
 
 HB.end.
 
-HB.factory Record Choice_isDioid (d : Order.disp_t) D of Choice D := {
+HB.factory Record Choice_isDioid (d : Order.disp_t) D & Choice D := {
   zero : D;
   add : D -> D -> D;
   one : D;
@@ -179,8 +179,8 @@ HB.factory Record Choice_isDioid (d : Order.disp_t) D of Choice D := {
   oner_neq0 : one != zero;
 }.
 
-HB.builders Context d D of Choice_isDioid d D.
-HB.instance Definition _ := GRing.isSemiRing.Build D addA addC add0d
+HB.builders Context d D & Choice_isDioid d D.
+HB.instance Definition _ := GRing.isNzSemiRing.Build D addA addC add0d
   mulA mul1d muld1 mulDl mulDr mul0d muld0 oner_neq0.
 HB.instance Definition _ := SemiRing_isDioid.Build d D adddd.
 HB.end.
@@ -231,9 +231,9 @@ Proof. move=> ac bd; exact/(le_trans (led_mul2r _ ac))/led_mul2l. Qed.
 End DioidTheory.
 
 #[short(type="comDioidType")]
-HB.structure Definition ComDioid d := { D of GRing.ComSemiRing D & Dioid d D }.
+HB.structure Definition ComDioid d := { D of GRing.ComNzSemiRing D & Dioid d D }.
 
-HB.factory Record POrder_isComDioid d D of Order.POrder d D := {
+HB.factory Record POrder_isComDioid d D & Order.POrder d D := {
   zero : D;
   add : D -> D -> D;
   one : D;
@@ -251,7 +251,7 @@ HB.factory Record POrder_isComDioid d D of Order.POrder d D := {
   le_def : forall (a b : D), (a <= b) = (add a b == b);
 }.
 
-HB.builders Context d D of POrder_isComDioid d D.
+HB.builders Context d D & POrder_isComDioid d D.
 
 Lemma muld1 : right_id one mul.
 Proof. by move=> x; rewrite mulC mul1d. Qed.
@@ -269,7 +269,7 @@ HB.instance Definition _ := GRing.SemiRing_hasCommutativeMul.Build D mulC.
 
 HB.end.
 
-HB.factory Record Choice_isComDioid (d : Order.disp_t) D of Choice D := {
+HB.factory Record Choice_isComDioid (d : Order.disp_t) D & Choice D := {
   zero : D;
   add : D -> D -> D;
   one : D;
@@ -286,7 +286,7 @@ HB.factory Record Choice_isComDioid (d : Order.disp_t) D of Choice D := {
   oner_neq0 : one != zero;
 }.
 
-HB.builders Context d D of Choice_isComDioid d D.
+HB.builders Context d D & Choice_isComDioid d D.
 
 Lemma muld1 : right_id one mul.
 Proof. by move=> x; rewrite mulC mul1d. Qed.
@@ -306,7 +306,7 @@ HB.end.
 
 #[short(type="subDioidType")]
 HB.structure Definition SubDioid d (D : dioidType d) (S : pred D) d' :=
-  { U of GRing.SubSemiRing D S U & @Order.SubPOrder d D S d' U & Dioid d' U }.
+  { U of GRing.SubNzSemiRing D S U & @Order.SubPOrder d D S d' U & Dioid d' U }.
 
 #[short(type="subDioidLatticeType")]
 HB.structure Definition SubDioidLattice d (D : dioidLatticeType d) S d' :=
@@ -325,9 +325,9 @@ HB.structure Definition SubDioidTBLattice d (D : dioidLatticeType d) S d' :=
   { U of @SubDioid d D S d' U & @Order.TBLattice d' U }.
 
 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 := {}.
+    & GRing.SubNzSemiRing 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.
+HB.builders Context d D S d' U & SubSemiRing_SubPOrder_isSubDioid d D S d' U.
 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).
@@ -336,13 +336,13 @@ HB.instance Definition _ := SemiRing_POrder_isDioid.Build d' U adddd le_def.
 HB.end.
 
 HB.factory Record SubChoice_isSubDioid d (D : dioidType d) S (d' : Order.disp_t)
-    U of SubChoice D S U := {
+    U & SubChoice D S U := {
   semiring_closed_subproof : semiring_closed S;
 }.
 
 HB.builders Context d (D : dioidType d) S d' U
-  of SubChoice_isSubDioid d D S d' U.
-HB.instance Definition _ := GRing.SubChoice_isSubSemiRing.Build D S U
+  & SubChoice_isSubDioid d D S d' U.
+HB.instance Definition _ := GRing.SubChoice_isSubNzSemiRing.Build D S U
   semiring_closed_subproof.
 HB.instance Definition _ := Order.SubChoice_isSubPOrder.Build d D S d' U.
 HB.instance Definition _ := SubSemiRing_SubPOrder_isSubDioid.Build d D S d' U.
@@ -353,22 +353,22 @@ HB.structure Definition SubComDioid d (D : comDioidType d) (S : pred D) d' :=
   {U of @SubDioid d D S d' U & ComDioid d' U}.
 
 HB.factory Record SubComSemiRing_SubPOrder_isSubComDioid d (D : comDioidType d)
-  S (d' : Order.disp_t) U of GRing.SubComSemiRing D S U & @Order.SubPOrder d D S
+  S (d' : Order.disp_t) U & GRing.SubComNzSemiRing D S U & @Order.SubPOrder d D S
   d' U := {}.
 
 HB.builders Context d D S d' U
-  of SubComSemiRing_SubPOrder_isSubComDioid d D S d' U.
+  & SubComSemiRing_SubPOrder_isSubComDioid d D S d' U.
 HB.instance Definition _ := SubSemiRing_SubPOrder_isSubDioid.Build d D S d' U.
 HB.end.
 
 HB.factory Record SubChoice_isSubComDioid d (D : comDioidType d) S
-    (d' : Order.disp_t) U of SubChoice D S U := {
+    (d' : Order.disp_t) U & SubChoice D S U := {
   semiring_closed_subproof : semiring_closed S
 }.
 
 HB.builders Context d (D : comDioidType d) S d' U
-  of SubChoice_isSubComDioid d D S d' U.
-HB.instance Definition _ := GRing.SubChoice_isSubComSemiRing.Build D S U
+  & SubChoice_isSubComDioid d D S d' U.
+HB.instance Definition _ := GRing.SubChoice_isSubComNzSemiRing.Build D S U
   semiring_closed_subproof.
 HB.instance Definition _ := Order.SubChoice_isSubPOrder.Build d D S d' U.
 HB.instance Definition _ := SubSemiRing_SubPOrder_isSubDioid.Build d D S d' U.