for L being non empty right_complementable add-associative right_zeroed addLoopStr
for p being Polynomial of L holds deg (- p) = deg p by POLYNOM4:8;