proposition: Lemma padding_BitString_into_ByteString : forall l, padding (BitString_into_ByteString l) = NPeano.modulo (length l) 8.
proof: Proof. induction l. simpl; eauto. simpl length. destruct (Peano_dec.eq_nat_dec (NPeano.modulo (length l) 8) 7). - rewrite NatModulo_S_Full. simpl. unfold ByteString_push. destruct (Peano_dec.eq_nat_dec (padding (BitString_into_ByteString l)) 7). simpl; eauto. exfalso. rewrite IHl in n; congruence. eauto. - rewrite NatModulo_S_Not_Full; eauto. unfold NPeano.Nat.modulo in IHl |- *; rewrite <- IHl. simpl. unfold ByteString_push. unfold NPeano.modulo, NPeano.Nat.modulo in IHl, n; rewrite <- IHl in n. destruct (Peano_dec.eq_nat_dec (padding (BitString_into_ByteString l)) 7); simpl; eauto. congruence. 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