proposition: Lemma ByteString_transform_padding_0_left : forall str1 str2, padding str1 = 0 -> padding (transform str1 str2) = padding str2.
proof: Proof. intros * H; rewrite transform_padding_eq, H. apply NPeano.Nat.mod_small. destruct str2; assumption. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat CertifiedExtraction.Extraction.BinEncoders.Basics Coq.Lists.List Bedrock.Word Program Nomega