for L being non degenerated right_complementable add-associative right_zeroed distributive doubleLoopStr
for p being monic Polynomial of L
for q being Polynomial of L st deg p > deg q holds
p - q is monic