def internal_nat_mul_comm

bend-mathlib@0.8.1.0 · algebra.bend:103

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

103def internal_nat_mul_comm(x: Nat, y: Nat) -> {Nat.mul(x, y) == Nat.mul(y, x) : Nat}:
104  MNat.mul_comm(x, y)