for b being Ordinal holds b -leading_coeff 1 = 1