proposition: Lemma OneCToZ_wnot_neg: forall (sz : nat) (w : word sz), OneCToZ (wnot w) = - OneCToZ w.
proof: Proof. destruct w. + reflexivity. + unfold OneCToZ. rewrite wmsb_wnot. destruct (wmsb _ _); repeat match goal with | _ => reflexivity | _ => progress simpl | _ => progress rewrite ?Bool.negb_involutive, ?wnot_involutive | [ |- context[if ?t then ?a else ?b] ] => destruct (if t then a else b) end. 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