# Equivalence Relations COQ

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.

• If you want to mark a question as resolved, please click on the little checkmark on the left of an answer. This way it is much more visible and convenient.
– Trebor
May 17 at 3:01

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.

You'll have to finish the admit. sections.