law op_left_comm

bend-mathlib@0.8.1.0 · algebra.bend:22

import Base

22# Left commutation from associativity and commutativity.
23law op_left_comm:
24  for ~A: Data
25  for ~op: A -> A -> A
26  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
27  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
28  for +a: A
29  for +b: A
30  for +c: A
31  {op(a, op(b, c)) == op(b, op(a, c)) : A}