let m, n be Nat; :: thesis: ( 2 * m <= n implies card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m) )
assume A1: 2 * m <= n ; :: thesis: card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)

now :: thesis: card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)

per cases ( m = 0 or m > 0 ) ;

suppose A2: m = 0 ; :: thesis: card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)

then n choose m = 1 by NEWTON:19;
then (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m) = 1 by A2, XCMPLX_1:60;
hence card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m) by A2, Th24; :: thesis: verum

end;

suppose A3: m > 0 ; :: thesis: card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m)

A4: m <= m + m by NAT_1:11;
then reconsider nm = n - m as Nat by A1, NAT_1:21, XXREAL_0:2;
reconsider m1 = m - 1 as Nat by A3, NAT_1:20;
set n9 = n ! ;
set m9 = m ! ;
set nm19 = (nm + 1) ! ;
set nm9 = nm ! ;
m <= n by A1, A4, XXREAL_0:2;
then A5: n choose m = (n !) / ((m !) * (nm !)) by NEWTON:def 3;
A6: 2 * (m1 + 1) <= n by A1;
set m19 = m1 ! ;
A7: 1 / ((m1 !) * ((nm + 1) !)) = ((m1 + 1) * 1) / (((m1 !) * ((nm + 1) !)) * (m1 + 1)) by XCMPLX_1:91
.= m / (((nm + 1) !) * ((m1 !) * (m1 + 1)))
.= m / (((nm + 1) !) * ((m1 + 1) !)) by NEWTON:15
.= - ((- m) / (((nm + 1) !) * (m !))) by XCMPLX_1:190 ;
1 / ((m !) * (nm !)) = ((nm + 1) * 1) / (((m !) * (nm !)) * (nm + 1)) by XCMPLX_1:91
.= (nm + 1) / ((m !) * ((nm !) * (nm + 1)))
.= (nm + 1) / ((m !) * ((nm + 1) !)) by NEWTON:15 ;
then A8: (1 / ((m !) * (nm !))) - (1 / ((m1 !) * ((nm + 1) !))) = ((nm + 1) / ((m !) * ((nm + 1) !))) + ((- m) / ((m !) * ((nm + 1) !))) by A7
.= ((nm + 1) + (- m)) / ((m !) * ((nm + 1) !)) by XCMPLX_1:62
.= ((n + 1) - (2 * m)) / ((m !) * ((nm !) * (nm + 1))) by NEWTON:15
.= (1 * ((n + 1) - (2 * m))) / (((m !) * (nm !)) * (nm + 1))
.= (1 / ((m !) * (nm !))) * (((n + 1) - (2 * m)) / (nm + 1)) by XCMPLX_1:76 ;
m1 <= m1 + ((1 + m1) + 1) by NAT_1:11;
then A9: m1 <= n by A1, XXREAL_0:2;
n - m1 = nm + 1 ;
then A10: n choose m1 = (n !) / ((m1 !) * ((nm + 1) !)) by A9, NEWTON:def 3;
((n !) / ((m !) * (nm !))) - ((n !) / ((m1 !) * ((nm + 1) !))) = ((n !) * (1 / ((m !) * (nm !)))) - ((n !) / ((m1 !) * ((nm + 1) !))) by XCMPLX_1:99
.= ((n !) * (1 / ((m !) * (nm !)))) - ((n !) * (1 / ((m1 !) * ((nm + 1) !)))) by XCMPLX_1:99
.= (n !) * ((1 / ((m !) * (nm !))) - (1 / ((m1 !) * ((nm + 1) !))))
.= (n !) * ((1 / ((m !) * (nm !))) * (((n + 1) - (2 * m)) / (nm + 1))) by A8
.= ((n !) * (1 / ((m !) * (nm !)))) * (((n + 1) - (2 * m)) / (nm + 1))
.= (((n !) * 1) / ((m !) * (nm !))) * (((n + 1) - (2 * m)) / (nm + 1)) by XCMPLX_1:74 ;
hence card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m) by A5, A10, A6, Th28; :: thesis: verum

end;

end;

end;

hence card (Domin_0 (n,m)) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m) ; :: thesis: verum