That's a lot of manual effort to save just a tiny bit of thinking. The first digit is the largest digit among the first N-1 digits. The second digit is the largest digit to the right of the first digit up to and including the Nth digit. That's it.
Hi! Yes, I talk about this a little bit at the end and I solve Part 2 the normal way. This is a toy example that I did for fun. The objective was to introduce people to Program Construction and show how you can use formal methods to derive correct programs. Whether the juice is worth the squeeze is a judgement call that you make depending on how critical the software you are writing is.
It was a fun read though, and obviously this exercise is not about efficiency so much as exploring an interesting idea.