theorem Th37: :: POLYDIFF:37

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L holds (p || ((len p) -' 1)) + (Leading-Monomial p) = p