Theorem binaryEvalPaddedBytesAligned : forall bs a (Hnz : 0 <> a),
  length (binaryEvalPaddedBytes bs a Hnz) mod a = 0.
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.
