proposition: Lemma padding_eq_mod_8 : forall b, padding b = NPeano.modulo (length_ByteString b) 8.
proof: Proof. intros. rewrite (ByteString_into_BitString_eq b). unfold length_ByteString. rewrite !padding_BitString_into_ByteString. intros; rewrite <- NPeano.Nat.add_mod_idemp_r; eauto. rewrite (fun c => proj2 (NPeano.Nat.mod_divides (8 * _) 8 c)); eauto. rewrite <- plus_n_O, NPeano.Nat.mod_mod; eauto. 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