proposition: Lemma mod_eq_sym : Symmetric mod_eq.
proof: Proof. repeat intro. destruct H as [q H]. exists (-q). rewrite Zopp_mult_distr_l_reverse. rewrite <- H. ring. Qed.
imports: Arith ZArith RelationClasses Type_class_definition Lia ZArith Znumtheory