proposition: Lemma OneC_plus_comm {sz}: forall (w1 w2: word sz), w1 ^1+ w2 = w2 ^1+ w1.
proof: Proof. unfold OneC_plus; intros; rewrite Z.add_comm. destruct_eqdec; congruence. 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