The right hand is rendered as \(\Sigma z{:}\N.\, \I(\N,y+z+1,x)\) in intuitionistic type theory, and we take this as definition of relation \(&gt;\). (\(+\) is defined by recursive equations, \(\I\) is the identity type construction). Now all the properties of \(&gt;\) are determined by the mentioned introduction and elimination and computation rules for \(\N\).