let a be Ordinal; :: thesis: 1 -leading_coeff a = a
not 1 in 1 ;
hence 1 -leading_coeff a = a div^ (exp (1,0)) by ORDINAL5:def 10
.= a div^ 1 by ORDINAL2:43
.= a by ORDINAL3:71 ;
:: thesis: verum