Suggestion: Clarify the redundancy in theorem `Nat.le_succ_of_le` proof

[FlyCloudC]

Thank you for writing this book! I've learned a lot from it.

I have the following question:

In section 8.4.2.1, the theorem Nat.le_succ_of_le has the same type as Nat.le.step. Why not just write:

theorem Nat.le_succ_of_le : n ≤ m → n ≤ m + 1 := .step

If this is only to show readers more of the proof-writing process, it would be better to point this out explicitly, so that readers won’t be confused.