Require Export GeoCoq.Elements.OriginalProofs.euclidean_tactics.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_equalitysymmetric : 
   forall A B, 
   eq B A ->
   eq A B.
Proof.
(* Goal: forall (A B : @Point Ax) (_ : @eq Ax B A), @eq Ax A B *)
intros.
(* Goal: @eq Ax A B *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @eq Ax A B *)
assert (eq A B) by (conclude cn_equalitytransitive).
(* Goal: @eq Ax A B *)
close.
Qed.

End Euclid.
