def nbits_eq
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/xbits.bend:107
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as Xbits
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as S
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
107def nbits_eq(+k: List<&2, U32>) -> {X.nbits(k) == S.bits(k) : Nat}:
108 Equal.cong(Nat, Nat, z => Nat.sub(Nat.mul(8n, z), 1n), X.len(k), C.length(U32, k), len_eq(k))