fact: Definition OneC_plus_wplus sz := forall w1 w2: word sz, OneC_plus w1 w2 = w1 ^+ w2 ^+ split2 _ _ (zext w1 sz ^+ zext w2 sz).
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