proposition: Lemma OneC_plus_wnot {sz}: forall w, w ^1+ (wnot w) = wones sz.
proof: Proof. unfold OneC_plus; intros. rewrite OneCToZ_wnot_neg. replace (_ + _) with 0 by ring. destruct_eqdec; try congruence. - apply wnot_wzero_wones. - apply wnot_inj. rewrite wnot_wones_wzero; assumption. - apply ZToOneC_zero. 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