proposition: Corollary numBytes_ByteString_enqueue_ByteString : forall bs bs', padding bs = 0 -> numBytes (ByteString_enqueue_ByteString bs bs') = numBytes bs + numBytes bs'.
proof: Proof. intros. pose proof (length_ByteString_enqueue_ByteString bs bs') as H'; unfold length_ByteString in H'. rewrite padding_ByteString_enqueue_ByteString, H, !plus_O_n, padding_mod_8 in H'. omega. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Formats.ByteBuffer Coq.Strings.String Coq.Vectors.Vector Fiat.Narcissus.Formats.WordOpt Fiat.Common.Equality