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