proposition: Lemma wmsb_wnot': forall (n : nat) (w : word n) (b : bool), wmsb (wnot w) (negb b) = negb (wmsb w b).
proof: Proof. induction w; simpl; intros. * reflexivity. * rewrite IHw; reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing