Commit 2025-09-30 15:31 4243cfd7
View on Github →feat(Data/Nat/Init): n.AtLeastTwo implies NeZero (n - 1) (#29410)
Add an instance for NeZero (n - 1) deduced from n.AtLeastTwo.
feat(Data/Nat/Init): n.AtLeastTwo implies NeZero (n - 1) (#29410)
Add an instance for NeZero (n - 1) deduced from n.AtLeastTwo.