let m be Nat; :: thesis: for i being Integer st m divides i holds
i div m divides i
let i be Integer; :: thesis: ( m divides i implies i div m divides i )
assume A1: m divides i ; :: thesis: i div m divides i
per cases ( m <> 0 or m = 0 ) ;
suppose A2: m <> 0 ; :: thesis: i div m divides i
take m ; :: according to INT_1:def 3 :: thesis: i = (i div m) * m
i div m = i / m by A1, Th6;
hence i = (i div m) * m by A2, XCMPLX_1:87; :: thesis: verum
end;
suppose m = 0 ; :: thesis: i div m divides i
hence i div m divides i by A1, INT_1:48; :: thesis: verum
end;
end;