Theorem ENat.toNat_le_of_le_coe

Modification history

2026-07-17 11:15

Mathlib/Data/ENat/Basic.lean

chore(Data/ENat): replace `coe` with `natCast` in lemma names (#41140) …

Deleted ENat.toNat_le_of_le_coe View on Github →

2024-06-30 23:36

Mathlib/Data/ENat/Basic.lean

feat(ENat/Basic): add more `simp`/`gcongr` lemmas (#13651)

Added ENat.toNat_le_of_le_coe View on Github →