Positive (P): trait % Basic operators on natural numbers, % starting from 1 includes DecimalLiterals (P for N), TotalOrder (P) introduces 1: -> P succ: P -> P __+__, __*__: P, P -> P asserts P generated by 1, succ forall x, y: P x + 1 == succ(x); x + succ(y) == succ(x + y); x*1 == x; x*succ(y) == x + (x*y); x < succ(x) implies NaturalOrder (P for N, 1 for 0) P generated by 1, + converts +, *, <=, >=, <, >[Table of Contents] [Index]