proposition: Lemma ByteString_push_char_id_right : forall (chars : list char) (bs : ByteString), padding bs = 0 -> fold_right ByteString_push_char bs chars = {| front := WO; paddingOK := ByteString_id_subproof; byteString := chars ++ (byteString bs) |}.
proof: Proof. destruct bs; simpl; intros; subst. induction chars; simpl. - f_equal; eauto using le_uniqueness_proof. - rewrite IHchars. rename a into c. pose proof (shatter_word c); simpl in *; pose proof (shatter_word (wtl c)); simpl in *; pose proof (shatter_word (wtl (wtl c))); simpl in *; pose proof (shatter_word (wtl (wtl (wtl c)))); simpl in *; pose proof (shatter_word (wtl (wtl (wtl (wtl c))))); simpl in *; pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl c)))))); simpl in *; pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl (wtl c))))))); simpl in *; pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl (wtl (wtl c)))))))); pose proof (shatter_word (wtl (wtl (wtl (wtl (wtl (wtl (wtl (wtl c))))))))); simpl in *. rewrite H, H0, H1, H2, H3, H4, H5, H6, H7; simpl. rewrite !ByteString_push_char_WS. rewrite !ByteString_push_word_WS. simpl. unfold ByteString_push at 8; simpl. unfold ByteString_push at 7; simpl. unfold ByteString_push at 6; simpl. unfold ByteString_push at 5; simpl. unfold ByteString_push at 4; simpl. unfold ByteString_push at 3; simpl. unfold ByteString_push at 2; simpl. unfold ByteString_push at 1; simpl. f_equal. eapply le_uniqueness_proof. 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