Library Coq.Arith.Cantor
Implementation of the Cantor pairing and its inverse function
Bijections between
nat * nat and
nat
Cantor pairing
to_nat
Cantor pairing inverse of_nat
of_nat is the left inverse for to_nat
to_nat is injective
to_nat is the left inverse for of_nat
of_nat is injective
Polynomial specifications of to_nat
to_nat is non-decreasing in (the sum of) pair components