def internal_nat_add_assoc

bend-mathlib@0.8.1.0 · algebra.bend:88

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

88def internal_nat_add_assoc(x: Nat, y: Nat, z: Nat) -> {Nat.add(Nat.add(x, y), z) == Nat.add(x, Nat.add(y, z)) : Nat}:
89  MNat.add_assoc(x, y, z)