proposition: Lemma wordToN_combine: forall sz1 sz2 (w1: word sz1) (w2: word sz2), wordToN (combine w1 w2) = wordToN w1 + Npow2 sz1 * wordToN w2.
proof: Proof. induction w1; simpl; intros. - destruct (wordToN w2); reflexivity. - rewrite IHw1; destruct b, (wordToN w1), (Npow2 n), (wordToN w2); reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing