投票問題：\(A\) が \(p\) 票・\(B\) が \(q\) 票（\(p > q\)）の開票で、途中ずっと \(A\) が多い並びの数 \(N(p,q) = \binom{p+q-1}{q} - \binom{p+q-1}{q-1} = \frac{p-q}{p+q}\binom{p+q}{q}\)（差の形と比の形）。数え上げの漸化式を満たす \(N\) があれば、という条件付きの形で示す。

1 二項係数の補題

\(n\) 個から \(a\) 個を選ぶ数と \(b = n - a\) 個を選ぶ数は等しい。

2 比の形の準備

差の形から比の形へは、次の自然数の計算だけを使います（\(n = N(p,q)\)・\(u, v, t\) は二項係数）。

3 主定理

投票で \(A\) が \(p\) 票・\(B\) が \(q\) 票（\(p > q\)）のとき、開票の途中ずっと \(A\) が \(B\) より多い並びの数を \(N(p, q)\) とします。ここでは \(N\) を、数え上げの漸化式を満たす関数として仮定します（存在は示しません）。したがって主定理は「そのような \(N\) があれば」という条件付きの形です。
漸化式：\(N(p+1, 0) = 1\)。\(p \le q + 1\) なら \(N(p, q+1) = 0\)。\(q < p\) なら、最後の1票が \(A\) か \(B\) かで分けて \(N(p+1, q+1) = N(p, q+1) + N(p+1, q)\)。
閉じた形は \(N(p, q) = \binom{p+q-1}{q} - \binom{p+q-1}{q-1}\)（\(r = q - 1\)・\(m = p + q - 1\) と置いて、引き算を使わず足し算の形で述べます）。
Dform … \(\begin{cases} \forall p \in \mathbb{M} . \forall q \in \mathbb{M} . N ( p ) ( q ) \in \mathbb{M} \\ \forall p \in \mathbb{M} . N ( ( p + 1 ) ) ( 0 ) = 1 \\ \forall p \in \mathbb{M} . \forall q \in \mathbb{M} . ( p \le q + 1 \Longrightarrow N ( p ) ( ( q + 1 ) ) = 0 ) \\ \forall p \in \mathbb{M} . \forall q \in \mathbb{M} . ( q < p \Longrightarrow N ( ( p + 1 ) ) ( ( q + 1 ) ) = N ( p ) ( ( q + 1 ) ) + N ( ( p + 1 ) ) ( q ) ) \end{cases} , p , r , m \in \mathbb{M} , p + r = m , r + 1 \le p \Longrightarrow N ( p ) ( ( r + 1 ) ) + ( m \mathrm{C} r ) = m \mathrm{C} ( ( r + 1 ) )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，choose𝕄 ，Lsym ，Pc

4 比の形

差の形（Dform）から、\(q \ge 1\) のとき \(N(p,q) = \frac{p-q}{p+q}\binom{p+q}{q}\) を割り算を使わない形 \((p+q)\,N(p,q) = (p-q)\binom{p+q}{q}\) で述べます（\(p = q + k\) として \(p - q = k\)）。\(q = 0\) のときも成り立ちます。
\(\begin{cases} \forall p \in \mathbb{M} . \forall q \in \mathbb{M} . N ( p ) ( q ) \in \mathbb{M} \\ \forall p \in \mathbb{M} . N ( ( p + 1 ) ) ( 0 ) = 1 \\ \forall p \in \mathbb{M} . \forall q \in \mathbb{M} . ( p \le q + 1 \Longrightarrow N ( p ) ( ( q + 1 ) ) = 0 ) \\ \forall p \in \mathbb{M} . \forall q \in \mathbb{M} . ( q < p \Longrightarrow N ( ( p + 1 ) ) ( ( q + 1 ) ) = N ( p ) ( ( q + 1 ) ) + N ( ( p + 1 ) ) ( q ) ) \end{cases} , p , q , k \in \mathbb{M} , p = q + k \Longrightarrow ( p + q ) \cdot N ( p ) ( q ) = k \cdot ( ( p + q ) \mathrm{C} q )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，choose𝕄 ，Pc ，Ralg ，Dform