natural-arithmetic-0.1.2.0: Arithmetic of natural numbers

Arithmetic.Plus

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

Zero plus any number is equal to the original number.

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

Any number plus zero is equal to the original number.

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

Addition is commutative.

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

Addition is associative.