Agda cong doubut? (The position of lemma have different meaning)

Question

we have

+-comm : ∀ (m n : ℕ) → m + n ≡ n + m
+-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

and want to prove

+-swap' : ∀(m n p : ℕ) → m + (n + p) ≡ n + (m + p)

Here is what my first good try:

+-swap' : ∀(m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap' m n p =
begin m + (n + p)
≡⟨ sym (+-assoc m n p) ⟩
    (m + n) + p
≡⟨ +-comm (m + n) p ⟩
    p + (m + n)
≡⟨ sym (+-assoc p m n) ⟩
    (p + m) + n 
≡⟨ +-comm (p + m)  n ⟩
    n + (p + m)
≡⟨ cong (n +_) (+-comm p m) ⟩
    n + (m + p)
∎

And I want to simple it like this:

+-swap : ∀(m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p =
begin
m + (n + p)
≡⟨ sym (+-assoc m n p) ⟩ 
    (m + n) + p
≡⟨ cong ((+-comm m n) +_) p ⟩ -- the wrong line
    (n + m) + p
≡⟨ +-assoc n m p ⟩
    n + (m + p)
∎

However this time I got:

m + n ≡ n + m !=< _A_224 → _B_226 of type Set
when checking that the expression +-comm m n has type
_A_224 → _B_226

So what's the difference? For me I use the same pattern as the good one. Because I am so new to this topic. I also try ⟨ cong (+-comm m n) (p +_) ⟩ which like ⟨ cong (n +_) (+-comm p m) ⟩ but it don't work.

Answer 1

In the https://plfa.github.io/Induction.

A relation is said to be a congruence for a given function if it is preserved
by applying that function. If e is evidence that x ≡ y, then cong f e is 
evidence that f x ≡ f y, for any function f

After I understand this. I change to this

+-swap : ∀(m n p : ℕ) → m + (n + p) ≡ n + (m + p)
+-swap m n p =
begin
m + (n + p)
≡⟨ sym (+-assoc m n p) ⟩ 
    (m + n) + p
≡⟨ cong (_+ p) (+-comm m n) ⟩   -- need to compute
    (n + m) + p
≡⟨ +-assoc n m p ⟩
n + (m + p)
∎

The lemma here is (+-comm m n). the function will be (_+ p). May be it is helpful. I just keep my solution here.