proposition: Lemma ZToOneC_nonzero {sz} : forall z: Z, ZToOneC z <> wzero (S (S sz)).
proof: Proof. red; intros. unfold ZToOneC in *. pose proof (normalizeZ_rangeN (S sz) z); destruct (normalizeZ _ _) in *; match goal with | _ => eapply wones_not_wzero; eassumption | [ H: _ = wzero _ |- _ ] => rewrite ?wnot_waddmsb in H; apply (f_equal (@wcountones _)) in H; rewrite wcountones_wzero, wcountones_waddmsb in H; simpl in H end. - apply wcountones_zero in H; apply (f_equal (@wordToN _)) in H; rewrite wordToN_posToWord, wordToN_wzero in H by assumption; discriminate. - 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