Theorem PNat.one_lt_of_lt

Modification history

2024-04-28 14:16
Mathlib/Data/PNat/Basic.lean
feat(PNat/Basic): add three lemmas (#12479) …
Added PNat.one_lt_of_ltView on Github →