diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 612fc718b..baa80edc7 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -399,7 +399,7 @@ private definition pair_nat.lt : nat × nat → nat × nat → Prop := measure p
 private definition pair_nat.lt.wf : well_founded pair_nat.lt :=
 intro_k (measure.wf pr₂) 20  -- Remark: we use intro_k to be able to execute gcd efficiently in the kernel
 instance pair_nat.lt.wf -- Remark: instance will not be saved in .olean
-infixl `≺`:50 := pair_nat.lt
+infixl [local] `≺`:50 := pair_nat.lt
 
 private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) :=
 mod_lt (succ_pos y₁)