let k, l, m, n be natural Number ; :: thesis: ( k mod n = 0 & l = k - (m * n) implies l mod n = 0 )
assume that
A1: k mod n = 0 and
A2: l = k - (m * n) ; :: thesis: l mod n = 0

per cases ( n = 0 or n <> 0 ) ;

suppose n = 0 ; :: thesis: l mod n = 0

hence l mod n = 0 by A1, A2; :: thesis: verum

end;

suppose n <> 0 ; :: thesis: l mod n = 0

then consider t being Nat such that
A3: k = (n * t) + 0 and
A4: 0 < n by A1, Def2;
A5: l = (n * (t - m)) + 0 by A2, A3;

now :: thesis: not t < m + 0

assume t < m + 0 ; :: thesis: contradiction
then t - m < 0 by XREAL_1:19;
then l < n * 0 by A4, A5, XREAL_1:68;
hence contradiction ; :: thesis: verum

end;

then t - m is Element of NAT by NAT_1:21;
hence l mod n = 0 by A4, A5, Def2; :: thesis: verum

end;

end;