proposition: Lemma wordToN_bound {size} (w: Word.word size): (wordToN w < Npow2 size)%N.
proof: Proof. Opaque N.mul. induction size. - rewrite (shatter_word_0 w); reflexivity. - destruct (shatter_word_S w) as (b & [ w' ? ]); subst. destruct b; simpl. rewrite <- N.add_1_r. auto using N.double_above. auto using N_lt_double_lt, N.double_above. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing