I am also unfamiliar and trying to solve proofs relative to the topic Relations and Divisibility but I would like to solve such COQ proof theorems. I am not quite sure how to solve proofs like this for example :
Require Import Arith.
Definition relation (X Y : Type) := X -> Y -> Prop.
Definition reflexive {X: Type} (R: relation X X) := forall a : X, R a a.
Definition transitive {X: Type} (R: relation X X) := forall a b c : X, (R a b) -> (R b c) -> (R a c).
Definition symmetric {X: Type} (R: relation X X) := forall a b : X, (R a b) -> (R b a).
Definition antisymmetric {X: Type} (R: relation X X) := forall a b : X, (R a b) -> (R b a) -> a = b.
Definition equivalence {X:Type} (R: relation X X) := (reflexive R) /\ (symmetric R) /\ (transitive R).
Definition congruence (a b c : Z) := (a | (b - c)).
Lemma relations_ex : forall a : Z, equivalence (congruence a).
Proof.
EDIT :
1 goal
a, x, y, H1 : Z
H2 : x - y = H1 * a
______________________________________(1/1)
y - x = -1 * (a * H1)
unfold symmetric, congruence.
intros x y H.
unfold congruence in *.
destruct H as [H1 H2].
exists (-H1).
rewrite Z.opp_eq_mul_m1.
rewrite Z.mul_comm.
rewrite Z.mul_assoc.
rewrite Z.mul_comm.
rewrite <- Z.opp_mul_distr_l.
reflexivity.