Enlightening article trying to verify leftpad (+2 other small functions) in a range of theorem provers: https://www.hillelwayne.com/post/theorem-prover-showdown/