Leanで試そうとした結果、証明が正しくないことがわかったって結論でええやろ。