removed some unnecessary algebraic (commutativity, assoc) lemmas, after the reordering of last commit