let g, m be Nat; :: thesis: for i being Integer st g divides i & g divides m holds
i / m = (i div g) / (m div g)
let i be Integer; :: thesis: ( g divides i & g divides m implies i / m = (i div g) / (m div g) )
assume that
A1: g divides i and
A2: g divides m ; :: thesis: i / m = (i div g) / (m div g)

per cases ( g = 0 or m = 0 or ( g <> 0 & m <> 0 ) ) ;

suppose g = 0 ; :: thesis: i / m = (i div g) / (m div g)

hence i / m = (i div g) / (m div g) by A1; :: thesis: verum

end;

suppose A4: m = 0 ; :: thesis: i / m = (i div g) / (m div g)

( i / 0 = 0 & (i div g) / (0 div g) = 0 ) by XCMPLX_1:49;
hence i / m = (i div g) / (m div g) by A4; :: thesis: verum

end;

suppose that A5: g <> 0 and
A6: m <> 0 ; :: thesis: i / m = (i div g) / (m div g)

g <= m by A2, A6, INT_2:27;
then A7: m div g <> 0 by A5, NAT_2:13;
( i mod g = 0 & m mod g = 0 ) by A1, A2, A5, INT_1:62;
then ( m div g = m / g & i div g = i / g ) by PEPIN:63;
then i * (m div g) = m * (i div g) ;
hence i / m = (i div g) / (m div g) by A6, A7, XCMPLX_1:94; :: thesis: verum

end;

end;