proposition: Lemma wmsb_wnot: forall (n : nat) (w : word (S n)), wmsb (wnot w) true = negb (wmsb w true).
proof: Proof. intros; destruct (shatter_word_S w) as (b & [ w' ? ]); subst. simpl; apply wmsb_wnot'. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing