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:70;
n ! > 0 * ((m ! ) * (nm ! )) ;
then (n ! ) / ((m ! ) * (nm ! )) > 0 by A2, XREAL_1:83;
hence n choose m > 0 by A1, NEWTON:def 3; :: thesis: verum