succ-free induction on nat

Stream: Is there code for X?

[Kevin Buzzard]

Do we have an induction principle on nat which is defeq to nat.rec but which talks about n+1 instead of n.succ? I was developing teaching materials and I noticed that sometimes I can't do induction, ring, I have to do induction, simp, ring.

import tactic

example (n : ℕ) : (n.succ : ℚ)^2 = n^2+2*n+1 := by ring -- fails (as does simp, but simp, ring works)

[Reid Barton]

I have used this too, https://github.com/rwbarton/lean-omin/blob/master/src/for_mathlib/nat.lean

[Reid Barton]

maybe it should have some equational lemmas I guess, apparently I didn't need them