proposition: Lemma normalizeZ_noop : forall p z, OneC_InRange p z -> normalizeZ p z = z.
proof: Proof. intros * (? & ?). unfold normalizeZ; intros; repeat match goal with | _ => progress rewrite ?N2Z.inj_mul, ?N2Z.inj_sub by eauto using Npow2_ge_one | _ => progress (simpl (Z.of_N _); simpl (Npow2 _)) end; set (Z.of_N _) in *. rewrite Z.mod_small by lia. ring. 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 AlignedByteString Permutation