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

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

suppose A2: n <> 0 ; :: thesis: (k + l) div n = (k div n) + (l div n)

then A3: k = (n * (k div n)) + 0 by A1, INT_1:59;
A4: ex t being Nat st
( l = (n * t) + (l mod n) & l mod n < n ) by A2, Def2;
l = (n * (l div n)) + (l mod n) by A2, INT_1:59;
then k + l = (n * ((k div n) + (l div n))) + (l mod n) by A3;
hence (k + l) div n = (k div n) + (l div n) by A4, Def1; :: thesis: verum

end;

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

hence (k + l) div n = (k div n) + (l div n) ; :: thesis: verum

end;

end;