def internal_nat_zero_add

bend-mathlib@0.8.1.0 · algebra.bend:94

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

94def internal_nat_zero_add(x: Nat) -> {Nat.add(0n, x) == x : Nat}:
95  MNat.zero_add(x)