chore: move Int.coe_nat_strictMono (#13197)

Author: Ruben-VandeVelde

Mathlib/Algebra/Group/Int.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jeremy Avigad
 -/
 import Mathlib.Algebra.Group.Nat
-import Mathlib.Order.Monotone.Basic
 import Mathlib.Tactic.Common
 
 #align_import data.int.basic from "leanprover-community/mathlib"@"00d163e35035c3577c1c79fa53b68de17781ffc1"
@@ -19,8 +18,7 @@ See note [foundational algebra order theory].
 -/
 
 assert_not_exists Ring
--- TODO
--- assert_not_exists DenselyOrdered
+assert_not_exists DenselyOrdered
 
 open Nat
 
@@ -79,9 +77,6 @@ lemma natAbs_pow (n : ℤ) (k : ℕ) : Int.natAbs (n ^ k) = Int.natAbs n ^ k :=
   · rw [_root_.pow_succ, natAbs_mul, Nat.pow_succ, ih, Nat.mul_comm]
 #align int.nat_abs_pow Int.natAbs_pow
 
-theorem coe_nat_strictMono : StrictMono (· : ℕ → ℤ) := fun _ _ ↦ Int.ofNat_lt.2
-#align int.coe_nat_strict_mono Int.coe_nat_strictMono
-
 section Multiplicative
 
 open Multiplicative

Mathlib/Algebra/GroupPower/IterateHom.lean

@@ -4,9 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yury Kudryashov
 -/
 import Mathlib.Algebra.Group.Int
-import Mathlib.Algebra.Group.Nat
 import Mathlib.GroupTheory.GroupAction.Opposite
-import Mathlib.Tactic.Common
+import Mathlib.Logic.Function.Iterate
 
 #align_import algebra.hom.iterate from "leanprover-community/mathlib"@"792a2a264169d64986541c6f8f7e3bbb6acb6295"
 
@@ -27,6 +26,8 @@ We also prove formulas for iterates of add/mul left/right.
 homomorphism, iterate
 -/
 
+assert_not_exists DenselyOrdered
+assert_not_exists Ring
 
 open Function
 
@@ -192,5 +193,3 @@ theorem Commute.function_commute_mul_right (h : Commute a b) :
 #align add_commute.function_commute_add_right AddCommute.function_commute_add_right
 
 end Semigroup
-
-assert_not_exists Ring

Mathlib/Algebra/Order/Group/Int.lean

@@ -34,6 +34,9 @@ open Function Nat
 
 namespace Int
 
+theorem coe_nat_strictMono : StrictMono (· : ℕ → ℤ) := fun _ _ ↦ Int.ofNat_lt.2
+#align int.coe_nat_strict_mono Int.coe_nat_strictMono
+
 instance linearOrderedAddCommGroup : LinearOrderedAddCommGroup ℤ where
   __ := instLinearOrder
   __ := instAddCommGroup