for a, b being Ordinal holds b -leading_coeff <%a%> = <%(b -leading_coeff a)%>