let n, k be non zero Nat; :: thesis: ( n mod k > 0 implies n div k = (n - 1) div k )
assume A1: n mod k > 0 ; :: thesis: n div k = (n - 1) div k
( n = ((n div k) * k) + (n mod k) & n - 1 = (((n - 1) div k) * k) + ((n - 1) mod k) ) by NAT_D:2;
then ((n div k) * k) / k = ((((((n - 1) div k) * k) + ((n - 1) mod k)) + 1) - (n mod k)) / k
.= ((((((n - 1) div k) * k) + ((n mod k) - 1)) + 1) - (n mod k)) / k by A1, ND3
.= (n - 1) div k by XCMPLX_1:89 ;
hence n div k = (n - 1) div k by XCMPLX_1:89; :: thesis: verum