79210487

Date: 2024-11-21 09:25:38
Score: 0.5
Natty:
Report link

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.

Reasons:
  • Has code block (-0.5):
  • Single line (0.5):
  • Low reputation (0.5):
Posted by: Tragicus