proposition: Lemma wplus_wnot {sz}: forall w, wplus w (wnot w) = wones sz.
proof: Proof. unfold wplus, wordBin; intros. rewrite wordToN_wnot, wplus_wnot_1, <- wordToN_wones, NToWord_wordToN; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing