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.