proposition: Lemma wordToN_NToWord : forall sz w, exists k, (wordToN (NToWord sz w) = w - k * Npow2 sz /\ k * Npow2 sz <= w)%N.
proof: Proof. intros. destruct (wordToNat_natToWord sz (N.to_nat w)) as [ w' (Heq & side_condition) ]. exists (N.of_nat w'). rewrite NToWord_nat. rewrite wordToN_nat. split. - apply N2Nat.inj. rewrite Nat2N.id, N2Nat.inj_sub, N2Nat.inj_mul, Nat2N.id, Npow2_nat. assumption. - unfold N.le. rewrite N2Nat.inj_compare. rewrite <- nat_compare_le. rewrite N2Nat.inj_mul, Nat2N.id, Npow2_nat. assumption. 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