proposition: Lemma normalizeZ_rangeN : forall p z, match normalizeZ p z with | Z0 => True | Zpos x => (Npos x < Npow2 p)%N | Zneg x => (Npos x < Npow2 p)%N end.
proof: Proof. intros; destruct (normalizeZ_range p z). destruct (normalizeZ _ _); lia. 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