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