# Library GeoCoq.Elements.OriginalProofs.lemma_equalitysymmetric

Require Export GeoCoq.Elements.OriginalProofs.euclidean_tactics.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_equalitysymmetric :

∀ A B,

eq B A →

eq A B.

Proof.

intros.

assert (eq A A) by (conclude cn_equalityreflexive).

assert (eq A B) by (conclude cn_equalitytransitive).

close.

Qed.

End Euclid.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_equalitysymmetric :

∀ A B,

eq B A →

eq A B.

Proof.

intros.

assert (eq A A) by (conclude cn_equalityreflexive).

assert (eq A B) by (conclude cn_equalitytransitive).

close.

Qed.

End Euclid.