:: deftheorem defines -leading_coeff ORDINAL7:def 2 :
for a, b being Ordinal holds b -leading_coeff a = a div^ (exp (b,(b -exponent a)));