Equivalence Relations COQ

Question

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.

Answer 1

Here's a framework for getting started.

Lemma relations_ex : forall a : Z, equivalence (congruence a).
Proof.
  intros a.
  repeat split.
  - unfold reflexive, congruence.
    intros x.
    admit.
  - unfold symmetric, congruence.
    intros x y.
    admit.
  - unfold transitive, congruence.
    intros x y z.
    admit.
Admitted.

You'll have to finish the admit. sections.