let m, n be Nat; :: thesis: ( m <= n implies n choose m > 0 )
assume A1: m <= n ; :: thesis: n choose m > 0
then reconsider nm = n - m as Nat by NAT_1:21;
A2: (m !) * (nm !) > (m !) * 0 by XREAL_1:68;
n ! > 0 * ((m !) * (nm !)) ;
then (n !) / ((m !) * (nm !)) > 0 by A2, XREAL_1:81;
hence n choose m > 0 by A1, NEWTON:def 3; :: thesis: verum