proposition: Lemma wcountones_waddmsb {sz} : forall (w: word sz) b, wcountones (waddmsb w b) = wcountones (WS b w).
proof: Proof. induction w; simpl in *; intros. - reflexivity. - specialize (IHw b0). destruct b; destruct b0; simpl in *; rewrite IHw; reflexivity. 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