chore(algebra/order/monoid): move lemmas (#16176)

* move `with_top.coe_nat` to `algebra.order.monoid`, prove by `rfl`;
* move `with_top.nat_ne_top` and `with_top.top_ne_nat` to `algebra.order.monoid`;
* add `with_bot` versions.

src/algebra/order/monoid.lean

@@ -1094,6 +1094,10 @@ instance [canonically_linear_ordered_add_monoid α] :
   canonically_linear_ordered_add_monoid (with_top α) :=
 { ..with_top.canonically_ordered_add_monoid, ..with_top.linear_order }
 
+@[simp, norm_cast] lemma coe_nat [add_monoid_with_one α] (n : ℕ) : ((n : α) : with_top α) = n := rfl
+@[simp] lemma nat_ne_top [add_monoid_with_one α] (n : ℕ) : (n : with_top α) ≠ ⊤ := coe_ne_top
+@[simp] lemma top_ne_nat [add_monoid_with_one α] (n : ℕ) : (⊤ : with_top α) ≠ n := top_ne_coe
+
 /-- Coercion from `α` to `with_top α` as an `add_monoid_hom`. -/
 def coe_add_hom [add_monoid α] : α →+ with_top α :=
 ⟨coe, rfl, λ _ _, rfl⟩
@@ -1160,6 +1164,10 @@ with_top.coe_eq_one
 @[to_additive] protected lemma map_one {β} [has_one α] (f : α → β) :
   (1 : with_bot α).map f = (f 1 : with_bot β) := rfl
 
+@[norm_cast] lemma coe_nat [add_monoid_with_one α] (n : ℕ) : ((n : α) : with_bot α) = n := rfl
+@[simp] lemma nat_ne_bot [add_monoid_with_one α] (n : ℕ) : (n : with_bot α) ≠ ⊥ := coe_ne_bot
+@[simp] lemma bot_ne_nat [add_monoid_with_one α] (n : ℕ) : (⊥ : with_bot α) ≠ n := bot_ne_coe
+
 section has_add
 variables [has_add α] {a b c d : with_bot α} {x y : α}
 

src/data/nat/cast.lean

@@ -227,16 +227,6 @@ end mul_opposite
 namespace with_top
 variables [add_monoid_with_one α]
 
-@[simp, norm_cast] lemma coe_nat : ∀ (n : ℕ), ((n : α) : with_top α) = n
-| 0     := rfl
-| (n+1) := by { push_cast, rw [coe_nat n] }
-
-@[simp] lemma nat_ne_top (n : nat) : (n : with_top α) ≠ ⊤ :=
-by { rw [←coe_nat n], apply coe_ne_top }
-
-@[simp] lemma top_ne_nat (n : nat) : (⊤ : with_top α) ≠ n :=
-by { rw [←coe_nat n], apply top_ne_coe }
-
 lemma add_one_le_of_lt {i n : with_top ℕ} (h : i < n) : i + 1 ≤ n :=
 begin
   cases n, { exact le_top },