Require Export GeoCoq.Elements.OriginalProofs.lemma_TGsymmetric.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_TTorder : 
   forall A B C D E F G H, 
   TT A B C D E F G H ->
   TT C D A B E F G H.
Proof.
(* Goal: forall (A B C D E F G H : @Point Ax0) (_ : @TT Ax0 A B C D E F G H), @TT Ax0 C D A B E F G H *)
intros.
let Tf:=fresh in
assert (Tf:exists J, (BetS E F J /\ Cong F J G H /\ TG A B C D E J)) by (conclude_def TT );destruct Tf as [J];spliter.
(* Goal: @TT Ax0 C D A B E F G H *)
assert (TG C D A B E J) by (conclude lemma_TGsymmetric).
(* Goal: @TT Ax0 C D A B E F G H *)
assert (TT C D A B E F G H) by (conclude_def TT ).
(* Goal: @TT Ax0 C D A B E F G H *)
close.
Qed.

End Euclid.