let k, m, n be Nat; :: thesis: ( n <= m implies n div k <= m div k )
assume that
A1: n <= m and
A2: n div k > m div k ; :: thesis: contradiction
set r = (n div k) -' (m div k);
A3: (n div k) -' (m div k) = (n div k) - (m div k) by A2, XREAL_1:233;
then (n div k) -' (m div k) > (m div k) - (m div k) by A2, XREAL_1:9;
then (n div k) -' (m div k) >= 0 + 1 by NAT_1:13;
then k * ((n div k) -' (m div k)) >= k * 1 by XREAL_1:64;
then A4: (k * ((n div k) -' (m div k))) + (k * (m div k)) >= k + (k * (m div k)) by XREAL_1:6;

per cases ( k <> 0 or k = 0 ) ;

suppose A5: k <> 0 ; :: thesis: contradiction

then ex t2 being Nat st
( m = (k * (m div k)) + t2 & t2 < k ) by NAT_D:def 1;
then m < k + (k * (m div k)) by XREAL_1:6;
then m - (k * (n div k)) < (k + (k * (m div k))) - (k + (k * (m div k))) by A3, A4, XREAL_1:14;
then A6: m - (k * (n div k)) < 0 ;
ex t1 being Nat st
( n = (k * (n div k)) + t1 & t1 < k ) by A5, NAT_D:def 1;
then k * (n div k) <= n by NAT_1:11;
then m - n < (k * (n div k)) - (k * (n div k)) by A6, XREAL_1:13;
then m < 0 + n by XREAL_1:19;
hence contradiction by A1; :: thesis: verum

end;

suppose k = 0 ; :: thesis: contradiction

hence contradiction by A2; :: thesis: verum

end;

end;