Merge pull request #5 from DanGrayson/master

needed but trivial changes -- "apply pr2" doesn't work at my end.
op precat
stuck in op_op
need product from pullback
making it compile under 8.4, thanks to DanGrayson's help
simplified a proof, found by DanGrayson
merge with upstream changes