fact: Fixpoint waddmsb {sz} (w: word sz) msb : word (S sz) := match w with | WO => WS msb WO | @WS b sz w' => WS b (waddmsb w' msb) end.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing