def zero_vg
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/scalar3.bend:65
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar3.bend as Scalar3
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
65def zero_vg(+one: Nat, +h1: {one == 1n : Nat}) -> {K.valo(one, zeros()) == 0n : Nat}:
66 Equal.trans(Nat, K.valo(one, zeros()), LM.shn(32n, K.valo(one, Nil{})), 0n, K.run0(one, 32n, Nil{}), {==})