:: deftheorem defines mod^ ORDINAL3:def 7 :
for A, B being Ordinal holds A mod^ B = A -^ ((A div^ B) *^ B);