proposition: Lemma OneC_plus_assoc {sz}: forall (w1 w2 w3: word sz), w1 ^1+ (w2 ^1+ w3) = (w1 ^1+ w2) ^1+ w3.
proof: Proof. unfold OneC_plus; destruct sz; intros. - setoid_rewrite shatter_word_0; reflexivity. - destruct_eqdec; try congruence; try match goal with | [ H: ZToOneC _ = (wzero _) |- _ ] => destruct sz; [ | exfalso; eapply ZToOneC_nonzero; eassumption] end; change (wzero 1) with (WO~0) in *; repeat match goal with | [ w: word 1 |- _ ] => shatter_word w | [ b: bool |- _ ] => destruct b; try congruence end. rewrite !OneCToZ_ZToOneC; unfold ZToOneC. rewrite ?normalizeZ_add_normalizeZ_l, ?normalizeZ_add_normalizeZ_r. replace (OneCToZ w3 + (OneCToZ w1 + OneCToZ w2)) with (OneCToZ w1 + (OneCToZ w2 + OneCToZ w3)) by ring. reflexivity. 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