let m, n be Integer; :: thesis: (m * n) mod n = 0

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

suppose A1: n <> 0 ; :: thesis: (m * n) mod n = 0

hence (m * n) mod n = (m * n) - (((m * n) div n) * n) by INT_1:def 10
.= (m * n) - ([\((m * n) / n)/] * n) by INT_1:def 9
.= (m * n) - ([\m/] * n) by A1, XCMPLX_1:89
.= (m * n) - (m * n)
.= 0 ;
:: thesis: verum

end;

suppose n = 0 ; :: thesis: (m * n) mod n = 0

hence (m * n) mod n = 0 by INT_1:def 10; :: thesis: verum

end;

end;