let k, m be Nat; :: thesis: (k - m) mod m = k mod m
thus (k - m) mod m = (k + (m * (- 1))) mod m
.= k mod m by NAT_D:61 ; :: thesis: verum