let n, m be Nat; :: thesis: frac (m / n) = (m mod n) / n

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

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

hence frac (m / n) = frac 0
.= (m mod n) / n by A1 ;
:: thesis: verum

end;

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

then m = (n * (m div n)) + (m mod n) by NAT_D:2;
then (m / n) + 0 = (m div n) + ((m mod n) / n) by A2, XCMPLX_1:113;
hence frac (m / n) = (m mod n) / n ; :: thesis: verum

end;

end;