let m, n be Integer; :: thesis: ( frac (m / n) = (m mod n) / n & m mod n = n * (frac (m / n)) )

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

suppose A1: n = 0 ; :: thesis: ( frac (m / n) = (m mod n) / n & m mod n = n * (frac (m / n)) )

then T1: frac (m / n) = frac 0
.= (m mod n) / n by A1 ;
(frac (m / n)) * n = (n * (m mod n)) / n by A1;
thus ( frac (m / n) = (m mod n) / n & m mod n = n * (frac (m / n)) ) by A1, T1; :: thesis: verum

end;

suppose A2: n > 0 ; :: thesis: ( frac (m / n) = (m mod n) / n & m mod n = n * (frac (m / n)) )

set a = m;
set b = n;
reconsider b = n as non zero Integer by A2;
m mod b = m - (b * (m div b)) by INT_1:def 10
.= ((m / b) * b) - (b * (m div b)) by XCMPLX_1:87
.= (([\(m / b)/] + (frac (m / b))) * b) - (b * (m div b))
.= ((b * [\(m / b)/]) + (b * (frac (m / b)))) - (b * [\(m / b)/])
.= b * (frac (m / b)) ;
hence ( frac (m / n) = (m mod n) / n & m mod n = n * (frac (m / n)) ) by XCMPLX_1:89; :: thesis: verum

end;

suppose A2: n < 0 ; :: thesis: ( frac (m / n) = (m mod n) / n & m mod n = n * (frac (m / n)) )

set a = m;
set b = n;
reconsider b = n as non zero Integer by A2;
m mod b = m - (b * (m div b)) by INT_1:def 10
.= ((m / b) * b) - (b * (m div b)) by XCMPLX_1:87
.= (([\(m / b)/] + (frac (m / b))) * b) - (b * (m div b))
.= ((b * [\(m / b)/]) + (b * (frac (m / b)))) - (b * [\(m / b)/])
.= b * (frac (m / b)) ;
hence ( frac (m / n) = (m mod n) / n & m mod n = n * (frac (m / n)) ) by XCMPLX_1:89; :: thesis: verum

end;

end;