Lemma about the coercion `ℕ → with_bot ℕ`. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

theorem nat.cast_with_top (n : ℕ) :

theorem nat.cast_with_bot (n : ℕ) :

Lemma about the coercion ℕ → with_bot ℕ. #