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