mathlib3 documentation

data.nat.cast.with_top

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 : ) :