proposition: Lemma normalizeZ_add_normalizeZ_l {sz} : forall z1 z2, normalizeZ sz ((normalizeZ sz z2) + z1) = normalizeZ sz (z1 + z2).
proof: Proof. intros; rewrite Z.add_comm; apply normalizeZ_add_normalizeZ_r. 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