Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthantransitive.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_TTtransitive : 
   forall A B C D E F G H P Q R S, 
   TT A B C D E F G H -> TT E F G H P Q R S ->
   TT A B C D P Q R S.
Proof.
(* Goal: forall (A B C D E F G H P Q R S : @Point Ax0) (_ : @TT Ax0 A B C D E F G H) (_ : @TT Ax0 E F G H P Q R S), @TT Ax0 A B C D P Q R S *)
intros.
let Tf:=fresh in
assert (Tf:exists K, (BetS E F K /\ Cong F K G H /\ TG A B C D E K)) by (conclude_def TT );destruct Tf as [K];spliter.
let Tf:=fresh in
assert (Tf:exists J, (BetS A B J /\ Cong B J C D /\ Lt E K A J)) by (conclude_def TG );destruct Tf as [J];spliter.
let Tf:=fresh in
assert (Tf:exists L, (BetS P Q L /\ Cong Q L R S /\ TG E F G H P L)) by (conclude_def TT );destruct Tf as [L];spliter.
let Tf:=fresh in
assert (Tf:exists M, (BetS E F M /\ Cong F M G H /\ Lt P L E M)) by (conclude_def TG );destruct Tf as [M];spliter.
(* Goal: @TT Ax0 A B C D P Q R S *)
assert (eq K K) by (conclude cn_equalityreflexive).
(* Goal: @TT Ax0 A B C D P Q R S *)
assert (neq F K) by (forward_using lemma_betweennotequal).
(* Goal: @TT Ax0 A B C D P Q R S *)
assert (neq F M) by (forward_using lemma_betweennotequal).
(* Goal: @TT Ax0 A B C D P Q R S *)
assert (Out F K M) by (conclude_def Out ).
(* Goal: @TT Ax0 A B C D P Q R S *)
assert (Out F K K) by (conclude lemma_ray4).
(* Goal: @TT Ax0 A B C D P Q R S *)
assert (Cong G H F M) by (conclude lemma_congruencesymmetric).
(* Goal: @TT Ax0 A B C D P Q R S *)
assert (Cong F K F M) by (conclude lemma_congruencetransitive).
(* Goal: @TT Ax0 A B C D P Q R S *)
assert (eq K M) by (conclude lemma_layoffunique).
(* Goal: @TT Ax0 A B C D P Q R S *)
assert (Lt P L E K) by (conclude cn_equalitysub).
(* Goal: @TT Ax0 A B C D P Q R S *)
assert (Lt P L A J) by (conclude lemma_lessthantransitive).
(* Goal: @TT Ax0 A B C D P Q R S *)
assert (TG A B C D P L) by (conclude_def TG ).
(* Goal: @TT Ax0 A B C D P Q R S *)
assert (TT A B C D P Q R S) by (conclude_def TT ).
(* Goal: @TT Ax0 A B C D P Q R S *)
close.
Qed.

End Euclid.