chore: split Std.Data.Int.Lemmas (#534)

leanprover-community · Jan 23, 2024 · 6ee0731 · 6ee0731
1 parent d3ccd13
commit 6ee0731
Show file tree

Hide file tree

Showing 6 changed files with 1,048 additions and 1,031 deletions.
diff --git a/Std/Data/Int.lean b/Std/Data/Int.lean
@@ -2,3 +2,4 @@ import Std.Data.Int.Basic
 import Std.Data.Int.DivMod
 import Std.Data.Int.Gcd
 import Std.Data.Int.Lemmas
+import Std.Data.Int.Order
diff --git a/Std/Data/Int/DivMod.lean b/Std/Data/Int/DivMod.lean
@@ -3,7 +3,7 @@ Copyright (c) 2016 Jeremy Avigad. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad, Mario Carneiro
 -/
-import Std.Data.Int.Lemmas
+import Std.Data.Int.Order
 import Std.Tactic.Change
 
 /-!