law nat_mul_four

bend-mathlib@0.8.1.0 · algebra.bend:172

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

172# Nat multiplication's middle-four interchange (the same statement as MNat.mul_mul_mul_comm).
173law nat_mul_four:
174  for +a: Nat
175  for +b: Nat
176  for +c: Nat
177  for +d: Nat
178  {Nat.mul(Nat.mul(a, b), Nat.mul(c, d)) == Nat.mul(Nat.mul(a, c), Nat.mul(b, d)) : Nat}