def internal_nat_mul_assoc

bend-mathlib@0.8.1.0 · algebra.bend:100

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

100def internal_nat_mul_assoc(x: Nat, y: Nat, z: Nat) -> {Nat.mul(Nat.mul(x, y), z) == Nat.mul(x, Nat.mul(y, z)) : Nat}:
101  MNat.mul_assoc(x, y, z)