mathlib3

f004d327 - feat(data/nat): various lemmas (#1017)

feat(data/nat): various lemmas (#1017) * feat(data/nat): various lemmas * protect a definition * fixes * Rob's suggestions * Mario’s proof (Working offline, let’s see what Travis says) * minigolf