Def Nat.Upto.succ

Modification history

2022-12-14 15:48
Mathlib/Data/Nat/Upto.lean
feat port: Data.Nat.Upto (#1020) …
Added Nat.Upto.succView on Github →