let k, m be Nat; :: thesis: ( m <> 0 implies (k - m) div m = (k div m) - 1 )
assume AS: m <> 0 ; :: thesis: (k - m) div m = (k div m) - 1
thus (k - m) div m = (k + (m * (- 1))) div m
.= (k div m) + (- 1) by AS, NAT_D:61
.= (k div m) - 1 ; :: thesis: verum