:: deftheorem defines RED ARYTM_3:def 6 :
for a, b being natural Ordinal holds RED (a,b) = a div^ (a hcf b);