Type.Data.Num.Unary.Proof

data Nat x

data Pos x

natFromPos

addNat

addPosL

addPosR

mulNat

mulPos