let k, l, n be natural Number ; :: thesis: ( k mod n = 0 implies (k + l) mod n = l mod n )
assume A1: k mod n = 0 ; :: thesis: (k + l) mod n = l mod n

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

suppose A2: n = 0 ; :: thesis: (k + l) mod n = l mod n

hence (k + l) mod n = 0 by Def2
.= l mod n by A2, Def2 ;
:: thesis: verum

end;

suppose A3: n <> 0 ; :: thesis: (k + l) mod n = l mod n

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

end;

end;