proposition: Lemma wones_not_wzero {sz}: wones (S sz) <> wzero (S sz).
proof: Proof. rewrite <- wnot_wones_wzero; discriminate. 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