Data.Type.Natural.Class.Arithmetic

type family Zero nat :: nat where ...

type family One nat :: nat where ...

type S n

sZero

sOne

data ZeroOrSucc n

plusCong

plusCongR

plusCongL

succCong

multCong

multCongL

multCongR

minusCong

minusCongL

minusCongR

class IsPeano nat