let k, m be Nat; :: thesis: ( m <> 0 & (k + 1) mod m <> 0 implies (k + 1) div m = k div m )
assume C1: ( m <> 0 & (k + 1) mod m <> 0 ) ; :: thesis: (k + 1) div m = k div m
k + 1 = (((k + 1) div m) * m) + ((k + 1) mod m) by INT_1:59, C1
.= (((k + 1) div m) * m) + ((k mod m) + 1) by XLMOD02, C1 ;
then P1: ((((k + 1) div m) * m) + (k mod m)) - (k mod m) = (((k div m) * m) + (k mod m)) - (k mod m) by INT_1:59, C1;
thus (k + 1) div m = ((k div m) * m) / m by XCMPLX_1:89, C1, P1
.= k div m by XCMPLX_1:89, C1 ; :: thesis: verum