Lemma about the coercion ℕ → WithBot ℕ.

An orphaned lemma about casting from ℕ to WithBot ℕ, exiled here to minimize imports to data.rat.order for porting purposes.

instance instWellFoundedRelationWithTopNat : WellFoundedRelation (WithTop ℕ)

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

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