let n, k be Nat; for A, B being object st A <> B & n >= k holds
prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k)
let A, B be object ; ( A <> B & n >= k implies prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k) )
assume A1:
( A <> B & n >= k )
; prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k)
then A2:
card (Election (A,n,B,k)) = (n + k) choose n
by Th12;
A3:
( n + k >= k + 0 & (n + k) - k = n & n + k >= n )
by NAT_1:11;
A4:
(n + k) choose n > 0
by NAT_1:11, CATALAN2:26;
per cases
( n = k or n > k )
by A1, XXREAL_0:1;
suppose A5:
n = k
;
prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k)then
DominatedElection (
A,
n,
B,
k) is
empty
by Th18;
then
card (DominatedElection (A,n,B,k)) = 0
;
then
prob (DominatedElection (A,n,B,k)) = 0 / ((n + k) choose n)
by A2, RPR_1:def 1;
hence
prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k)
by A5;
verum end; suppose
n > k
;
prob (DominatedElection (A,n,B,k)) = (n - k) / (n + k)then A6:
card (DominatedElection (A,n,B,k)) =
((n - k) / (n + k)) * ((n + k) choose k)
by A1, Th27
.=
((n - k) / (n + k)) * ((n + k) choose n)
by A3, NEWTON:20
;
thus prob (DominatedElection (A,n,B,k)) =
(((n - k) / (n + k)) * ((n + k) choose n)) / ((n + k) choose n)
by A2, A6, RPR_1:def 1
.=
((n - k) / (n + k)) * (((n + k) choose n) / ((n + k) choose n))
by XCMPLX_1:74
.=
((n - k) / (n + k)) * 1
by A4, XCMPLX_1:60
.=
(n - k) / (n + k)
;
verum end; end;