Theorem ENat.top_ne_one

Modification history

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