We can build a curious kind of proof system for natural numbers and polynomials using the lens library.
My blog post with much more detail explaining the idea:
http://www.philipzucker.com/lens-as-a-divisibility-relation-goofin-off-with-the-algebra-of-types/