tower-of-hanoi proof that the towers of hanoi problem is solvable using the lean prover mostly an exercise in wrangling with vectors lol. it is absolutely possible to do this way more elegantly. possibly using arrays instead of vectors.