Require Export GeoCoq.Elements.OriginalProofs.euclidean_tactics.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_congruencesymmetric : 
   forall A B C D, 
   Cong B C A D ->
   Cong A D B C.
Proof.
(* Goal: forall (A B C D : @Point Ax) (_ : @Cong Ax B C A D), @Cong Ax A D B C *)
intros.
(* Goal: @Cong Ax A D B C *)
assert (Cong B C B C) by (conclude cn_congruencereflexive).
(* Goal: @Cong Ax A D B C *)
assert (Cong A D B C) by (conclude cn_congruencetransitive).
(* Goal: @Cong Ax A D B C *)
close.
Qed.

End Euclid.

