law op_right_comm

bend-mathlib@0.8.1.0 · algebra.bend:38

import Base

38# Right commutation from associativity and commutativity.
39law op_right_comm:
40  for ~A: Data
41  for ~op: A -> A -> A
42  for ~assoc: @x: A -> @y: A -> @z: A -> {op(op(x, y), z) == op(x, op(y, z)) : A}
43  for ~comm: @x: A -> @y: A -> {op(x, y) == op(y, x) : A}
44  for +a: A
45  for +b: A
46  for +c: A
47  {op(op(a, b), c) == op(op(a, c), b) : A}