theorem Th53: :: ORDINAL7:40

for a being Ordinal holds 1 -leading_coeff a = a