def internal_nat_add_comm

bend-mathlib@0.8.1.0 · algebra.bend:91

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

91def internal_nat_add_comm(x: Nat, y: Nat) -> {Nat.add(x, y) == Nat.add(y, x) : Nat}:
92  MNat.add_comm(x, y)