proposition: Lemma mod_eq_trans : Transitive mod_eq.
proof: Proof. intros q1 q2 q3 Hl Hr. destruct Hl as [q4 Hl], Hr as [q5 Hr]; exists (q4 + q5). rewrite Zmult_plus_distr_l; rewrite <- Hl; rewrite <- Hr; ring. Qed.
imports: Arith ZArith RelationClasses Type_class_definition Lia ZArith Znumtheory