feat(library/data/nat/{basic.lean,order.lean}): use migrate

library/data/nat/basic.lean

@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.nat.basic
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
 
 Basic operations on the natural numbers.
@@ -287,7 +285,7 @@ nat.cases_on n
              ... = succ (succ n' * m' + n') : add_succ)⁻¹)
           !succ_ne_zero))
 
-section
+section migrate_algebra
   open [classes] algebra
 
   protected definition comm_semiring [reducible] : algebra.comm_semiring nat :=
@@ -308,45 +306,11 @@ section
     zero_mul       := zero_mul,
     mul_zero       := mul_zero,
     mul_comm       := mul.comm⦄
-end
 
-section port_algebra
-  open [classes] algebra
   local attribute comm_semiring [instance]
-  theorem mul.left_comm : ∀a b c : ℕ, a * (b * c) = b * (a * c) := algebra.mul.left_comm
-  theorem mul.right_comm : ∀a b c : ℕ, (a * b) * c = (a * c) * b := algebra.mul.right_comm
-
   definition dvd (a b : ℕ) : Prop := algebra.dvd a b
   notation a ∣ b := dvd a b
 
-  theorem dvd.intro : ∀{a b c : ℕ} (H : a * c = b), a ∣ b := @algebra.dvd.intro _ _
-  theorem dvd.intro_left : ∀{a b c : ℕ} (H : c * a = b), a ∣ b := @algebra.dvd.intro_left _ _
-  theorem exists_eq_mul_right_of_dvd : ∀{a b : ℕ} (H : a ∣ b), ∃c, b = a * c :=
-    @algebra.exists_eq_mul_right_of_dvd _ _
-  theorem dvd.elim : ∀{P : Prop} {a b : ℕ} (H₁ : a ∣ b) (H₂ : ∀c, b = a * c → P), P :=
-    @algebra.dvd.elim _ _
-  theorem exists_eq_mul_left_of_dvd : ∀{a b : ℕ} (H : a ∣ b), ∃c, b = c * a :=
-    @algebra.exists_eq_mul_left_of_dvd _ _
-  theorem dvd.elim_left : ∀{P : Prop} {a b : ℕ} (H₁ : a ∣ b) (H₂ : ∀c, b = c * a → P), P :=
-    @algebra.dvd.elim_left _ _
-  theorem dvd.refl : ∀a : ℕ, a ∣ a := algebra.dvd.refl
-  theorem dvd.trans : ∀{a b c : ℕ},  a ∣ b → b ∣ c → a ∣ c := @algebra.dvd.trans _ _
-  theorem eq_zero_of_zero_dvd : ∀{a : ℕ},  0 ∣ a → a = 0 := @algebra.eq_zero_of_zero_dvd _ _
-  theorem dvd_zero : ∀a : ℕ, a ∣ 0 := algebra.dvd_zero
-  theorem one_dvd : ∀a : ℕ, 1 ∣ a := algebra.one_dvd
-  theorem dvd_mul_right : ∀a b : ℕ, a ∣ a * b := algebra.dvd_mul_right
-  theorem dvd_mul_left : ∀a b : ℕ, a ∣ b * a := algebra.dvd_mul_left
-  theorem dvd_mul_of_dvd_left : ∀{a b : ℕ} (H : a ∣ b) (c : ℕ), a ∣ b * c :=
-    @algebra.dvd_mul_of_dvd_left _ _
-  theorem dvd_mul_of_dvd_right : ∀{a b : ℕ} (H : a ∣ b) (c : ℕ), a ∣ c * b :=
-    @algebra.dvd_mul_of_dvd_right _ _
-  theorem mul_dvd_mul : ∀{a b c d : ℕ}, a ∣ b → c ∣ d → a * c ∣ b * d :=
-    @algebra.mul_dvd_mul _ _
-  theorem dvd_of_mul_right_dvd : ∀{a b c : ℕ}, a * b ∣ c → a ∣ c :=
-    @algebra.dvd_of_mul_right_dvd _ _
-  theorem dvd_of_mul_left_dvd : ∀{a b c : ℕ}, a * b ∣ c → b ∣ c :=
-    @algebra.dvd_of_mul_left_dvd _ _
-  theorem dvd_add : ∀{a b c : ℕ}, a ∣ b → a ∣ c → a ∣ b + c := @algebra.dvd_add _ _
-end port_algebra
-
+  migrate from algebra with nat replacing dvd → dvd
+end migrate_algebra
 end nat

library/data/nat/order.lean

@@ -1,8 +1,6 @@
 /-
 Copyright (c) 2014 Floris van Doorn. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-
-Module: data.nat.order
 Authors: Floris van Doorn, Leonardo de Moura, Jeremy Avigad
 
 The order relation on the natural numbers.
@@ -11,7 +9,9 @@ import data.nat.basic algebra.ordered_ring
 open eq.ops
 
 namespace nat
+
 /- lt and le -/
+
 theorem le_of_lt_or_eq {m n : ℕ} (H : m < n ∨ m = n) : m ≤ n :=
 or.elim H (take H1, le_of_lt H1) (take H1, H1 ▸ !le.refl)
 
@@ -141,7 +141,7 @@ le.intro !zero_add
 
 /- nat is an instance of a linearly ordered semiring -/
 
-section
+section migrate_algebra
   open [classes] algebra
   local attribute nat.comm_semiring [instance]
 
@@ -165,20 +165,16 @@ section
     mul_le_mul_of_nonneg_right := (take a b c H1 H2, mul_le_mul_right H1 c),
     mul_lt_mul_of_pos_left     := @mul_lt_mul_of_pos_left,
     mul_lt_mul_of_pos_right    := @mul_lt_mul_of_pos_right ⦄
-end
 
-section
-  open [classes] algebra
   local attribute nat.linear_ordered_semiring [instance]
 
   migrate from algebra with nat
     replacing has_le.ge → ge, has_lt.gt → gt
-    hiding pos_of_mul_pos_left, pos_of_mul_pos_right, lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right
-end
+    hiding add_pos_of_pos_of_nonneg,  add_pos_of_nonneg_of_pos,
+      add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg, le_add_of_nonneg_of_le,
+      le_add_of_le_of_nonneg, lt_add_of_nonneg_of_lt, lt_add_of_lt_of_nonneg,
+      lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right, pos_of_mul_pos_left, pos_of_mul_pos_right
 
-section port_algebra
-  open [classes] algebra
-  local attribute nat.linear_ordered_semiring [instance]
   theorem add_pos_left : ∀{a : ℕ}, 0 < a → ∀b : ℕ, 0 < a + b :=
     take a H b, @algebra.add_pos_of_pos_of_nonneg _ _ a b H !zero_le
   theorem add_pos_right : ∀{a : ℕ}, 0 < a → ∀b : ℕ, 0 < b + a :=
@@ -203,7 +199,7 @@ section port_algebra
     take a b H, @algebra.pos_of_mul_pos_left _ _ a b H !zero_le
   theorem pos_of_mul_pos_right : ∀{a b : ℕ}, 0 < a * b → 0 < a :=
     take a b H, @algebra.pos_of_mul_pos_right _ _ a b H !zero_le
-end port_algebra
+end migrate_algebra
 
 theorem zero_le_one : 0 ≤ 1 := dec_trivial
 theorem zero_lt_one : 0 < 1 := dec_trivial