refactor: Split off basic Nat file (#9551)

`Data.Nat.Basic` is currently made of two things:
* Basic lemmas that continue the theory in Std (and could belong there, really)
* Basic algebraic order instances

I need the first ones earlier in the algebraic order hierarchy, hence the split.

Part of #9411. Similar to #9443

Archive/Arithcc.lean

@@ -3,8 +3,8 @@ Copyright (c) 2020 Xi Wang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Xi Wang
 -/
+import Mathlib.Init.Data.Nat.Lemmas
 import Mathlib.Order.Basic
-import Mathlib.Data.Nat.Basic
 import Mathlib.Tactic.Common
 
 #align_import arithcc from "leanprover-community/mathlib"@"eb3595ed8610db8107b75b75ab64ab6390684155"

Mathlib.lean

@@ -1775,6 +1775,7 @@ import Mathlib.Data.Nat.Choose.Multinomial
 import Mathlib.Data.Nat.Choose.Sum
 import Mathlib.Data.Nat.Choose.Vandermonde
 import Mathlib.Data.Nat.Count
+import Mathlib.Data.Nat.Defs
 import Mathlib.Data.Nat.Digits
 import Mathlib.Data.Nat.Dist
 import Mathlib.Data.Nat.EvenOddRec

Mathlib/Algebra/GroupPower/CovariantClass.lean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad, Robert Y. Lewis, Yury G. Kudryashov
 -/
 import Mathlib.Algebra.GroupPower.Basic
 import Mathlib.Algebra.Order.Monoid.OrderDual
-import Mathlib.Data.Nat.Basic
+import Mathlib.Data.Nat.Defs
 import Mathlib.Tactic.Monotonicity.Attr
 
 /-!

Mathlib/Combinatorics/Quiver/Arborescence.lean

@@ -3,10 +3,10 @@ Copyright (c) 2021 David Wärn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: David Wärn
 -/
-import Mathlib.Order.WellFounded
-import Mathlib.Data.Nat.Basic
-import Mathlib.Combinatorics.Quiver.Subquiver
 import Mathlib.Combinatorics.Quiver.Path
+import Mathlib.Combinatorics.Quiver.Subquiver
+import Mathlib.Data.Nat.Defs
+import Mathlib.Order.WellFounded
 
 #align_import combinatorics.quiver.arborescence from "leanprover-community/mathlib"@"fc2ed6f838ce7c9b7c7171e58d78eaf7b438fb0e"
 

Mathlib/Control/Random.lean

@@ -3,15 +3,8 @@ Copyright (c) 2022 Henrik Böving. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Henrik Böving
 -/
-
-import Mathlib.Init.Order.Defs
-import Mathlib.Init.Data.Nat.Lemmas
-import Mathlib.Init.Data.Int.Order
 import Mathlib.Control.ULiftable
 import Mathlib.Data.Fin.Basic
-import Mathlib.Data.Nat.Basic
-import Mathlib.Order.ULift
-import Mathlib.Logic.Equiv.Functor
 
 #align_import control.random from "leanprover-community/mathlib"@"fdc286cc6967a012f41b87f76dcd2797b53152af"