law octets_len_drop

bend-osdev-bytes@0.1.1.1 · LAWS.bend:255

import Base
import bend-osdev-bytes@0.1.1.1/bytes.bend as B

255law octets_len_drop:
256  for +n: Nat
257  for +o: B.Octets
258  {B.Octets.len(B.Octets.drop(n, o)) == Nat.sub(B.Octets.len(o), n) : Nat}