[Agda] congruence, Preserves_2

[Serge D. Mechveliani]

People,
I have several beginner questions on the  \.-cong  field  in 
Standard library  (Agda-2.3.0.1 + lib-0.6).

For  m n : Nat,  p : n == 1,  build a proof for  (m + n) == (m + 1).

  p : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
  p m n p =  ?

(for this letter I replace 
     \bn -> Nat,  _\equiv_ -> ==,  _\~~_ -> ~~,  \. -> op,  \_2 -> _2,  
).


I.  The first successful expression I found was 

  p : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
  p m n p =  cong (_+_ m) p

But initially I tried the following.
  
II. In a general situation, one probably needs to apply  op-cong  from 
    Semigroup. I tried this approach for Nat.
IsCommutativeMonoid  has a field
                               op-cong : op Preserves_2 ~~ -> ~~ -> ~~
And I write
-------------------------------------------------
open import Data.Nat as Nat
open import Data.Nat.Properties as NatProp
...
p : (m : Nat) -> (n : Nat) -> n == 1 -> (m + n) == (m + 1)
p m n p =  +cong <what to set here ?>
  where
  isCSemir  = NatProp.isCommutativeSemiring
  +isComMon = IsCommutativeSemiring.+-isCommutativeMonoid isCSemir
  +comm = IsCommutativeMonoid.comm  +isComMon  -- Commutative == _+_

  +cong : _+_ Preserves_2 == -> == -> ==        -- what must be here?
  +cong = IsCommutativeMonoid.op-cong +isComMon
-------------------------------------------------

because I think that it is needed the instance of
                                      op Preserves_2 ~~ -> ~~ -> ~~
for  op -> Nat._+_,  ~~ -> ==.

The compiler reports
"Could not parse the application _+_ Preserves_2 ==
 when scope checking _+_ Preserves_2 ==
"
a) Please, how to fix this?
b) What is the type of this  +cong ?
c) For the value    ``+cong = IsCommutativeMonoid.op-cong  +isComMon'',
   can Agda itself show the type of  +cong  ?
   (such an info often occurs helpful).

d) What to set in the RHS of   p m n p =  ...   ?

Thank you in advance for explanation,

------
Sergei