def cv_4

bend-kit-collections@0.1.4.1 · nat_order.bend:189

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

189def cv_4(+a: Nat, +b: Nat, +c: Nat, +d: Nat) -> {d == F(L{0n, 0n, 0n, 0n, 1n}, VS{a, b, c, d}) : Nat}:
190  sy(Nat.add(d, 0n), d, MNat.add_zero(d))