plus commutes

plus_comm.idr

plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)

-- Base case
(O + m = m + O) <== plus_comm = 
    rewrite ((m + O = m) <== plusZeroRightNeutral) ==> 
            (O + m = m) in refl

-- Step case
(S k + m = m + S k) <== plus_comm =
    rewrite ((k + m = m + k) <== plus_comm) in
    rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
        refl
-- QED