proposition: Lemma wplus_wnot_1: forall (n : nat) (w : word n), wordToN w + (Npow2 n - 1 - wordToN w) = Npow2 n - 1.
proof: Proof. intros; pose proof (wordToN_bound (size := n) w); lia. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing