:: deftheorem defines Leading-Coefficient RATFUNC1:def 6 :
for L being non empty ZeroStr
for p being Polynomial of L holds Leading-Coefficient p = p . ((len p) -' 1);