Lemma about the coercion ℕ → WithBot ℕ.

An orphaned lemma about casting from ℕ to WithBot ℕ, exiled here during the port to minimize imports of Algebra.Order.Ring.Rat.

instance instWellFoundedRelationWithTopNat : WellFoundedRelation (WithTop ℕ)

Equations

• instWellFoundedRelationWithTopNat = { rel := fun (x1 x2 : WithTop ℕ) => x1 < x2, wf := instWellFoundedRelationWithTopNat._proof_1 }

theorem Nat.cast_withTop (n : ℕ) : ↑n = ↑n

theorem Nat.cast_withBot (n : ℕ) : ↑n = ↑n