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.
Mathlib.Data.Nat.Cast.WithTop
ℕ → WithBot ℕ
. #An orphaned lemma about casting from ℕ
to WithBot ℕ
,
exiled here to minimize imports to data.rat.order
for porting purposes.