Positive (P):[Table of Contents] [Index]trait% Basic operators on natural numbers, % starting from 1includesDecimalLiterals (PforN), TotalOrder (P)introduces1: -> P succ: P -> P __+__, __*__: P, P -> PassertsPgeneratedby1, succforallx, y: P x + 1 == succ(x); x + succ(y) == succ(x + y); x*1 == x; x*succ(y) == x + (x*y); x < succ(x)impliesNaturalOrder (PforN, 1for0) Pgeneratedby1, +converts+, *, <=, >=, <, >