proposition: Lemma OneCToZ_ZToOneC {sz}: forall z, OneCToZ (@ZToOneC sz z) = match sz with | O => 0 | S sz => normalizeZ sz z end.
proof: Proof. unfold ZToOneC; destruct sz; intros. - reflexivity. - pose proof (normalizeZ_rangeN sz z); destruct (normalizeZ _ _) eqn:? ; repeat match goal with | _ => solve [auto] | _ => solve [apply OneCToZ_wones] | _ => progress simpl | _ => progress unfold OneCToZ | _ => progress rewrite ?wmsb_waddmsb, ?wnot_waddmsb, ?wordToN_waddmsb | _ => progress rewrite ?N.add_0_r, ?wordToN_posToWord, ?wnot_involutive end. 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