proposition: Lemma normalizeZ_range : forall p z, OneC_InRange p (normalizeZ p z).
proof: Proof. split; repeat match goal with | _ => progress intros | _ => progress unfold normalizeZ | _ => progress ring_simplify | _ => progress autorewrite with normalizeZ | _ => progress rewrite ?N2Z.inj_mul, ?N2Z.inj_sub by eauto using Npow2_ge_one | _ => simpl (Z.of_N _) end. - apply Z_mod_lt. pose proof (Npow2_ge_one p); lia. - rewrite Z.lt_add_lt_sub_r. apply Z_mod_lt. pose proof (Npow2_ge_one p); 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