This is a great example. I also recall seeing refinement types (Liquid Haskell) used to prove termination of Euclids GCD.

For all I know, the GCD function buried in that gobbledygook could actually be calculating the LCM, and the proof could be of that.