proposition: Lemma wordToN_NToWord_idempotent: forall (sz : nat) (p : N), p < Npow2 sz -> wordToN (NToWord sz p) = p.
proof: Proof. intros; rewrite NToWord_nat. rewrite natToWordToN; rewrite N2Nat.id; auto. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing