work more on commutativity of multiplication. problem: keep forgetting that Coq has problems with n (op) value [value (op) n] is usually fine. lots of induction