diff --git a/Archive/Imo/Imo1988Q6.lean b/Archive/Imo/Imo1988Q6.lean
index e5a845afe1354..008184d1f84c1 100644
--- a/Archive/Imo/Imo1988Q6.lean
+++ b/Archive/Imo/Imo1988Q6.lean
@@ -3,6 +3,7 @@ Copyright (c) 2019 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johan Commelin
 -/
+import Mathlib.Algebra.Order.WithZero
 import Mathlib.Data.Nat.Prime
 import Mathlib.Data.Rat.Defs
 import Mathlib.Order.WellFounded
diff --git a/Archive/Imo/Imo1998Q2.lean b/Archive/Imo/Imo1998Q2.lean
index f8be7c974c0a1..351d4b1f58f21 100644
--- a/Archive/Imo/Imo1998Q2.lean
+++ b/Archive/Imo/Imo1998Q2.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Oliver Nash
 -/
 import Mathlib.Algebra.BigOperators.Order
+import Mathlib.Algebra.Order.Field.Basic
 import Mathlib.Data.Fintype.Prod
 import Mathlib.Data.Int.Parity
 import Mathlib.GroupTheory.GroupAction.Ring