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

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:29;
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, Th28; :: 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 Element of NAT by A1, NAT_1:21, XXREAL_0:2;
reconsider m1 = m - 1 as Element of 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:92
.= m / (((nm + 1) ! ) * ((m1 ! ) * (m1 + 1)))
.= m / (((nm + 1) ! ) * ((m1 + 1) ! )) by NEWTON:21
.= - ((- m) / (((nm + 1) ! ) * (m ! ))) by XCMPLX_1:191 ;
1 / ((m ! ) * (nm ! )) = ((nm + 1) * 1) / (((m ! ) * (nm ! )) * (nm + 1)) by XCMPLX_1:92
.= (nm + 1) / ((m ! ) * ((nm ! ) * (nm + 1)))
.= (nm + 1) / ((m ! ) * ((nm + 1) ! )) by NEWTON:21 ;
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:63
.= ((n + 1) - (2 * m)) / ((m ! ) * ((nm ! ) * (nm + 1))) by NEWTON:21
.= (1 * ((n + 1) - (2 * m))) / (((m ! ) * (nm ! )) * (nm + 1))
.= (1 / ((m ! ) * (nm ! ))) * (((n + 1) - (2 * m)) / (nm + 1)) by XCMPLX_1:77 ;
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:100
.= ((n ! ) * (1 / ((m ! ) * (nm ! )))) - ((n ! ) * (1 / ((m1 ! ) * ((nm + 1) ! )))) by XCMPLX_1:100
.= (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:75 ;
hence card (Domin_0 n,m) = (((n + 1) - (2 * m)) / ((n + 1) - m)) * (n choose m) by A5, A10, A6, Th32; :: thesis: verum

end;

end;

end;

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