proposition: Lemma wzero_S {sz} : wzero (S sz) = (wzero sz)~0.
proof: Proof. rewrite <- natToWord_wordToNat at 1. rewrite <- natToWord_wordToNat. f_equal. 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