diff --git a/algebra/ofe.v b/algebra/ofe.v
index 0e59c67278a40cf60c3b5b3cb321cca93b454e50..cf0dff4984d7968f1cbd15f7499e4d2d96705ce4 100644
--- a/algebra/ofe.v
+++ b/algebra/ofe.v
@@ -732,8 +732,11 @@ Proof. by intros x y. Qed.
 Instance leibnizC_leibniz A : LeibnizEquiv (leibnizC A).
 Proof. by intros x y. Qed.
 
-Canonical Structure natC := leibnizC nat.
 Canonical Structure boolC := leibnizC bool.
+Canonical Structure natC := leibnizC nat.
+Canonical Structure positiveC := leibnizC positive.
+Canonical Structure NC := leibnizC N.
+Canonical Structure ZC := leibnizC Z.
 
 (* Option *)
 Section option.