proposition: Lemma OneC_plus_wones {sz} : forall w, w <> (wzero sz) -> OneC_plus (wones sz) w = w.
proof: Proof. unfold OneC_plus; intros. pose proof (@wones_not_wzero sz). destruct (weqdec (wones _) _), (weqdec w (wzero sz)); try congruence. rewrite OneCToZ_wones; simpl. rewrite ZToOneC_OneCToZ; auto. 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