let x, y be Integer; :: thesis: ( x divides y implies y = (y div x) * x )
assume A1: x divides y ; :: thesis: y = (y div x) * x
then A2: y mod x = 0 by Lm10;

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

suppose x = 0 ; :: thesis: y = (y div x) * x

hence y = (y div x) * x by A1; :: thesis: verum

end;

suppose x <> 0 ; :: thesis: y = (y div x) * x

hence y = ((y div x) * x) + (y mod x) by INT_1:59
.= (y div x) * x by A2 ;
:: thesis: verum

end;

end;