You can not use your induction hypothesis because H
simplifies to n + n = m + m
while IHn
expects n + n = S m + S m
. In other words, the argument m
you want to feed the induction hypothesis changed, which is a symptom that you need to generalize over m
(with revert m
) before doing induction n
(actually you can just not introduce m
and H
before doing induction n
). Besides, you can also destruct
m
instead of doing an induction on it, the induction hypothesis IHm
is useless.