refactor(QR): Improve/golf LRL proofs (#1019)

* defs

* one-liners

* xdotp comms

* comm calcs

* comm simps

* rework x(pp) comm (xp)p

* rework x(pp) comm rx

* minor change lrlOp_eq

* change arg

Author: gloges