Multiplication (N):[Table of Contents] [Index]trait% Define the operator * in terms of 0, succ, and +includesAbelianMonoid (*for\circ, 1forunit, NforT), Addition (N)introduces1: -> N __*__: N, N -> Nassertsforallx, y: N 1 == succ(0); x * 0 == 0; x * succ(y) == x + (x * y)