add proof for associativity of multiplication. had to define three lemmas -- is there a better way? (assertions don't mix well with induction.) also, TODO: dependency graph for theorems and tactics used? that'd be super cool