let h, i, j be Nat; :: thesis: ( i divides j implies i divides j * h )
assume i divides j ; :: thesis: i divides j * h
then consider l being Nat such that
A1: j = i * l ;
(i * l) * h = i * (l * h) ;
hence i divides j * h by A1; :: thesis: verum