NaturalOrder (N):[Table of Contents] [Index]trait% The natural numbers with an orderingincludesEnumerable (N), TotalOrder (N)assertsforallx: N x < succ(x)impliesInfinite (N)forallx, y: N 0 <= x; x < succ(y) == x <= y; succ(x) < succ(y) == x < yconverts<=, >=, <, >