theorem :: INT_1:64

for r, s being Real st r / s is Integer holds
- [\(r / s)/] = [\((- r) / s)/]