Recognize numeric literals as Fin.succ in Fin n

Stream: mathlib4

[Jin Wei]

Hi there! I come across this pattern of lemmas needed in my proof.

lemma one (n : ℕ) : (1 : Fin (Nat.succ (Nat.succ n))) = Fin.succ 0 := rfl
lemma two (n : ℕ) : (2 : Fin (Nat.succ (Nat.succ (Nat.succ n)))) = Fin.succ 1 := rfl
...

I am wondering if there is some way to quantifier over the numeric literals 1, 2, etc and to have one lemma to deal them all.

[Kim Morrison]

You could probably write a simproc.

[Jin Wei]

Kim Morrison said:

You could probably write a simproc.

Thank you! I am not familiar with simproc but I will look it up.