proposition: Lemma wordToN_wzero {sz} : wordToN (wzero sz) = 0%N.
proof: Proof. intros; unfold wzero; rewrite natToWordToN. - reflexivity. - apply Npow2_gt_zero. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat List Bedrock.Word Coq.ZArith.ZArith Coq.micromega.Psatz NArith NArithRing