succ_le_succ theorem description incorrect

[ptrbman]

In the Advanced Multiplication World, Level 4/10, the description of the succ_le_succ theorem is described as

(x y : ℕ) (hx : MyNat.succ x ≤ MyNat.succ y) : x ≤ y

succ_le_succ x y is a proof that if succ x ≤ succ y then x ≤ y.

However, when applying the theorem, it instead mimics the rule found at (https://lovettsoftware.com/NaturalNumbers/InequalityWorld/Level8.lean.html):

For all naturals a and b, if a ≤ b, then succ a ≤ succ b.

In short, when applying it to
succ 0 ≤ succ a_1
I get
succ (succ 0) ≤ succ (succ a_1)
instead of
0 ≤ a_1

I do not know which is the intended solution but at least I am confused from reading the help.

[joneugster]

You are right that the analogue theorem in Lean Core is called Nat.le_of_succ_le_succ, so it would be better if the NNG renamed this lemma (which you proved in Level Inequality 9) from succ_le_succ to le_of_succ_le_succ to match the actual name in Lean!

If you want to make a PR, please do! Otherwise I'll just leave this open until I do the next cleanup round.