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