proposition: Lemma natToWordToN : forall n m, (N_of_nat m < Npow2 n)%N -> wordToN (natToWord n m) = N_of_nat m.
proof: Proof. intros; rewrite wordToN_nat, wordToNat_natToWord_idempotent by assumption. reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing