proposition: Lemma normalizeZ_add_1 : forall z z1 z2, (z1 + ((z2 + (z - 1)) mod (2 * z - 1) - (z - 1)) + (z - 1)) mod (2 * z - 1) = (z1 + z2 + (z - 1)) mod (2 * z - 1).
proof: Proof. intros. replace (z1 + ((z2 + (z - 1)) mod (2 * z - 1) - (z - 1)) + (z - 1)) with (z1 + (z2 + (z - 1)) mod (2 * z - 1)) by ring. rewrite Zplus_mod, Zmod_mod, <- Zplus_mod. f_equal; 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