proposition: Lemma wmsb_combine {sz} : forall (w : word (S sz)) b, exists w' : word sz, w = match eq_sym (Nat.add_1_r sz) in (_ = y) return (word y -> word (S sz)) with | eq_refl => fun w' => w' end (w' +^+ WS (wmsb w b) WO).
proof: Proof. induction sz; intros; destruct (shatter_word_S w) as (b' & [ w' ? ]); subst. - exists WO; pose proof (shatter_word_0 w'); subst; simpl. rewrite (UIP_nat _ _ (Nat.add_1_r 0) eq_refl); reflexivity. - specialize (IHsz w' b'); destruct IHsz as (w'' & Heq). simpl. exists (WS b' w''). change (WS b' w'' +^+ WS (wmsb w' b') WO) with (WS b' (w'' +^+ WS (wmsb w' b') WO)). eapply WS_match_eq_refl. rewrite Heq at 1. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing ZArith ZArithRing Program Coq.micromega.Psatz AlignedByteString Permutation