proposition: Lemma Zmod_plus_compat_l: forall x y z : Z, y %=z -> (x+y) %= (x+z).
proof: Proof. intros; unfold mod_eq in H; unfold mod_eq; rewrite Zminus_plus_simpl_l; exact H. Qed.
imports: Arith ZArith RelationClasses Type_class_definition Lia ZArith Znumtheory