The pairing function [1] is a way to implement bijections between `nat`

and `nat * nat`

. However, for the bijectivity proofs one requires facts about division, square roots, and floor function (which are tricky in Coq).

What is the most elegant Coq approach to write

- a function
`encode: nat * nat -> nat`

- a function
`decode: nat -> nat * nat`

- a lemma
`forall z, decode (encode z) = z`

- a lemma
`forall n, encode (decode n) = n`

possibly using `lia`

or `nia`

for automation?