a + b = b + a

-- Given the definition of plus:

-- total plus : (n, m : Nat) -> Nat
-- plus Z right        = right
-- plus (S left) right = S (plus left right)

total plus_comm : (left : Nat) -> (right : Nat) -> left + right = right + left

Please log in; otherwise your solution and progress won't be saved