Theorem ENat.one_ne_top

Modification history

2024-06-30 23:36
Mathlib/Data/ENat/Basic.lean
feat(ENat/Basic): add more `simp`/`gcongr` lemmas (#13651)
Added ENat.one_ne_topView on Github →