theorem Th41: :: NIVEN:43

for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p, q being Polynomial of L st deg p > deg q holds
deg (p - q) = deg p