proposition: Lemma wordToN_extend sz sz' : forall (w: word sz), wordToN (combine w (wzero sz')) = wordToN w.
proof: Proof. intros; rewrite (wordToN_combine sz sz'). rewrite wordToN_wzero; ring. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing