law len_mul

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/value.bend:523

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Li

523law len_mul:
524  for +x: List<&2, U32>
525  for +r: List<&2, U32>
526  for +n: Nat
527  for +hx: {Nat.is_le(len(x), n) == True{} : Bool}
528  {Nat.is_le(len(Li.mul(x, r)), Nat.add(len(r), n)) == True{} : Bool}