law op_right_comm_sym

bend-mathlib@0.8.1.0 · algebra.bend:322

import Base

322# Right commutation from associativity and commutativity, reversed to rewrite toward the simple side.
323law op_right_comm_sym:
324  for ~A: Data
325  for ~op: A -> A -> A
326  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
327  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
328  for +a: A
329  for +b: A
330  for +c: A
331  {op(op(a, c), b) == op(op(a, b), c) : A}