Theorem ENat.add_one_le_coe_iff

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.add_one_le_coe_iffView on Github →
2026-07-07 14:28
Mathlib/Data/ENat/Basic.lean
feat(Data/ENat/Basic): coe versions of `m + 1 ≤ n ↔ m < n` (#41372) …
Added ENat.add_one_le_coe_iffView on Github →