for R being non empty right_complementable add-associative right_zeroed well-unital distributive left_zeroed Euclidian doubleLoopStr holds R is PID