このチュートリアルめっちゃ重要だった。thm と verify コマンドと expand ヒントの使い方を覚えたぞ。
https://www.cs.utexas.edu/users/kaufmann/tutorial/rev3.html#top
expand のヒントの使い方を覚えたことで、11 以下のときは安全にヒットできることを示す定理がかけた。
https://gitlab.com/tojoqk/blackjack/-/commit/12733bfa51f3cc6c98d2b067bf3217f4e2a76145
https://mastodon.tojo.tokyo/@tojoqk/105606459763642932