:: deftheorem defines div INT_1:def 9 :
for i1, i2 being Integer holds i1 div i2 = [\(i1 / i2)/];