proposition: Lemma wplus_three {sz} : forall w1 w2 w3: word sz, w1 ^+ w2 ^+ w3 = NToWord sz (wordToN w1 + wordToN w2 + wordToN w3)%N.
proof: Proof. intros. rewrite !wordToN_nat, !NToWord_nat, !N2Nat.inj_add, !Nat2N.id. repeat rewrite wplus_alt; unfold wplusN, wordBinN. repeat match goal with | [ H: _ = _ |- _ ] => rewrite H; clear H | [ |- context[wordToNat (natToWord ?sz ?w)] ] => destruct (wordToNat_natToWord sz w) as [? [? ?]] end. replace (wordToNat w1 + wordToNat w2 - x * pow2 sz + wordToNat w3)%nat with (wordToNat w1 + wordToNat w2 + wordToNat w3 - x * pow2 sz)%nat by omega. apply drop_sub; omega. 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