Arithmetic.Plus

Documentation

zeroL :: m :=: (0 + m)

Zero plus any number is equal to the original number.

zeroR :: m :=: (m + 0)

Any number plus zero is equal to the original number.

commutative :: forall a b. (a + b) :=: (b + a)

Addition is commutative.

associative :: forall a b c. ((a + b) + c) :=: (a + (b + c))

Addition is associative.