proposition: Lemma wnot_wzero_wones : forall sz, wnot (wzero sz) = wones sz.
proof: Proof. intros; rewrite <- wnot_wones_wzero. apply wnot_involutive. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing