law mul_mul_mul_comm_sym

bend-mathlib@0.8.1.0 · nat.bend:4482

import Base

4482# Four-way regrouping of a product: (a * b) * (c * d) = (a * c) * (b * d), reversed to rewrite toward the simple side.
4483law mul_mul_mul_comm_sym:
4484  for a: Nat
4485  for b: Nat
4486  for c: Nat
4487  for d: Nat
4488  {Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) == Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) : Nat}