Require Export GeoCoq.Elements.OriginalProofs.lemma_congruencesymmetric.

Section Euclid.

Context `{Ax:euclidean_neutral}.

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

End Euclid.


