why this code is not working in agda?

Question

I am trying to prove commutative property over natural number on multiplication operation.

--proving comm over *
*comm : ∀ a b → (a * b) ≡ (b * a)
*comm zero b = sym (rightId* b)
*comm (suc a) b = {!!}

when i check goal I found that it is b + a * b ≡ b * suc a. So i proved this.

lemma*-swap : ∀ a b → a + a * b ≡ a * suc b

Now when i tried :

*comm : ∀ a b → (a * b) ≡ (b * a)
*comm zero b = sym (rightId* b)
*comm (suc a) b = lemma*-swap b a

This should work as it satisfied the goal but why this is not working?? Please suggest me where I am wrong.

Answer 1

b + a * b (the expression in the goal) and a + a * b (the expression in lemma*-swap) are distinct so applying lemma*-swap does not satisfy the goal.

You need to rewrite the induction hypothesis *comm a b to turn a * b into b * a in the goal so that the expression lemma*-swap b a can be used to discharge the goal.