why can't I rw here

Stream: new members

[Matt Yan]

Hi! I'm a new learner of LEAN and I'm following Kevin's incredible natural numbers tutorial,
Here's my simple goal: image.png
I'm tempted to use rw hk here but I can't, isn't succ k also a mynat?