For the first clause, check out

`sym`:

??> :doc sym
sym : (left = right) -> right = left
Symmetry of propositional equality
The function is Total

As for the second, you've overcomplicated things a bit.

To describe the (read: my) process a bit, consider

`?myPlusCommutative_rhs_2`:

myPlusCommutative (S k) m = ?myPlusCommutative_rhs_2

Since we know we want to recurse toward our base case (

`n = Z`):

myPlusCommutative (S k) m =
let inductiveHypothesis = myPlusCommutative k m in
rewrite inductiveHypothesis in
?myPlusCommutative_rhs_2

Now let's examine the type of

`myPlusCommutative_rhs_2`:

??> :t myPlusCommutative_rhs_2
k : Nat
m : Nat
inductiveHypothesis : plus k m = plus m k
_rewrite_rule : plus k m = plus m k
--------------------------------------
myPlusCommutative_rhs_2 : S (plus m k) = plus m (S k)

The type of

`myPlusCommutative_rhs_2` should look familiar:

??> :t plusSuccRightSucc
plusSuccRightSucc : (left : Nat) ->
(right : Nat) -> S (left + right) = left + S right

Thus we know how to fill in the hole:

myPlusCommutative (S k) m =
let inductiveHypothesis = myPlusCommutative k m in
rewrite inductiveHypothesis in
plusSuccRightSucc m k

As a matter of taste, I tend to avoid

`let`-ing too many variables, so I like to rewrite such code as follows:

myPlusCommutative (S k) m =
rewrite myPlusCommutative k m in
plusSuccRightSucc m k

Hope that helps!