let h, i, j be natural Number ; :: thesis: ( i divides j & i divides j + h implies i divides h )
assume that
A1: i divides j and
A2: i divides j + h ; :: thesis: i divides h
consider t being Nat such that
A3: j + h = i * t by A2;
consider u being Nat such that
A4: j = i * u by A1;

now :: thesis: ( i <> 0 implies i divides h )

assume A5: i <> 0 ; :: thesis: i divides h
then A6: h = (i * (h div i)) + (h mod i) by INT_1:59;
A7: j + ((i * (h div i)) + (h mod i)) = (i * (u + (h div i))) + (h mod i) by A4;
A8: h mod i < i by A5, Th1;
j + h = (i * t) + 0 by A3;
then h mod i = 0 by A6, A7, A8, NAT_1:18;
hence i divides h by A6; :: thesis: verum

end;

hence i divides h by A3; :: thesis: verum