How to reverse congr

Stream: lean4

[Locria Cyber]

theorem Nat.succ_symm : (Nat.succ x = Nat.succ y) -> x = y :=  by sorry

[Locria Cyber]

How do prove this

[David Renshaw]

theorem Nat.succ_symm : (Nat.succ x = Nat.succ y) -> x = y := succ.inj

[Marcus Rossel]

Just for context, since constructors of inductive types are injective there also exists an injection tactic which turns any hypothesis of the form MyType.cons a b ... = MyType.cons a' b' ... into a = a', b = b', ...

[Yakov Pechersky]

"reverse congr" is only possible if the function is injective. in this case, it is because it is an inductive constructor