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; :: thesis: verum

end;

end;