law op_comm3_sym

bend-mathlib@0.8.1.0 · algebra.bend:351

import Base

351# Three-way commutation from commutativity alone, reversed to rewrite toward the simple side.
352law op_comm3_sym:
353  for ~A: Data
354  for ~op: A -> A -> A
355  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
356  for +a: A
357  for +b: A
358  for +c: A
359  {op(c, op(b, a)) == op(op(a, b), c) : A}