law op_left_comm_sym

bend-mathlib@0.8.1.0 · algebra.bend:308

import Base

308# Left commutation from associativity and commutativity, reversed to rewrite toward the simple side.
309law op_left_comm_sym:
310  for ~A: Data
311  for ~op: A -> A -> A
312  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
313  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
314  for +a: A
315  for +b: A
316  for +c: A
317  {op(b, op(a, c)) == op(a, op(b, c)) : A}