let n, m, k be Nat; :: thesis: ( n <= m implies (m --> k) | n = n --> k )
assume n <= m ; :: thesis: (m --> k) | n = n --> k
then n c= m by NAT_1:39;
then n /\ m = n by XBOOLE_1:28;
hence (m --> k) | n = n --> k by FUNCOP_1:12; :: thesis: verum