proposition: Lemma normalizeZ_add_normalizeZ_r {sz} : forall z1 z2, normalizeZ sz (z1 + (normalizeZ sz z2)) = normalizeZ sz (z1 + z2).
proof: Proof. 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 _)) | _ => set (Z.of_N _) end. f_equal; apply normalizeZ_add_1. 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