proposition: Lemma wordToN_waddmsb: forall b (sz : nat) (w : word sz), wordToN (waddmsb w b) = wordToN w + (if b then Npow2 sz else 0).
proof: Proof. induction w; repeat match goal with | _ => ring | _ => reflexivity | _ => progress simpl | _ => rewrite <- !N.add_1_r | [ H: bool |- _ ] => destruct H | [ H: _ |- _ ] => rewrite H end. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing