proposition: Lemma wordToN_wones : forall sz, wordToN (wones sz) = Npow2 sz - 1.
proof: Proof. induction sz. - reflexivity. - simpl; rewrite IHsz. pose proof (Npow2_ge_one sz); lia. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing