proposition: Lemma wordToN_bound_wmsb_false: forall (sz : nat) (w : word (S sz)) b, wmsb w b = false -> (wordToN w < Npow2 sz)%N.
proof: Proof. induction sz. - intros; shatter_word w; simpl in *; subst; reflexivity. - intros * Heq; destruct (shatter_word_S w) as (b' & [ w' ? ]); subst; simpl in *. specialize (IHsz w' b' Heq). destruct b'; lia. 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