Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglesreflexive.
Require Export GeoCoq.Elements.OriginalProofs.lemma_angleorderrespectscongruence.
Require Export GeoCoq.Elements.OriginalProofs.lemma_crossbar.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_angleordertransitive : 
   forall A B C D E F P Q R, 
   LtA A B C D E F -> LtA D E F P Q R ->
   LtA A B C P Q R.
Proof.
(* Goal: forall (A B C D E F P Q R : @Point Ax0) (_ : @LtA Ax0 A B C D E F) (_ : @LtA Ax0 D E F P Q R), @LtA Ax0 A B C P Q R *)
intros.
let Tf:=fresh in
assert (Tf:exists U V W, (BetS U W V /\ Out Q P U /\ Out Q R V /\ CongA D E F P Q W)) by (conclude_def LtA );destruct Tf as [U[V[W]]];spliter.
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA P Q W D E F) by (conclude lemma_equalanglessymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (neq D E) by (forward_using lemma_angledistinct).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (neq E D) by (conclude lemma_inequalitysymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (neq E F) by (forward_using lemma_angledistinct).
(* Goal: False *)
assert (neq Q U) by (conclude lemma_raystrict).
let Tf:=fresh in
assert (Tf:exists G, (Out E D G /\ Cong E G Q U)) by (conclude lemma_layoff);destruct Tf as [G];spliter.
(* Goal: @LtA Ax0 A B C P Q R *)
assert (neq Q W) by (forward_using lemma_angledistinct).
let Tf:=fresh in
assert (Tf:exists J, (Out E F J /\ Cong E J Q W)) by (conclude lemma_layoff);destruct Tf as [J];spliter.
(* Goal: @LtA Ax0 A B C P Q R *)
assert (nCol D E F) by (conclude lemma_equalanglesNC).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA D E F D E F) by (conclude lemma_equalanglesreflexive).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA D E F G E J) by (conclude lemma_equalangleshelper).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA G E J D E F) by (conclude lemma_equalanglessymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA G E J P Q W) by (conclude lemma_equalanglestransitive).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (eq W W) by (conclude cn_equalityreflexive).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Out Q W W) by (conclude lemma_ray4).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA G E J U Q W) by (conclude lemma_equalangleshelper).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (nCol G E J) by (conclude lemma_equalanglesNC).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (nCol U Q W) by (conclude lemma_equalanglesNC).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Triangle G E J) by (conclude_def Triangle ).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Triangle U Q W) by (conclude_def Triangle ).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Cong G J U W) by (conclude proposition_04).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (eq W W) by (conclude cn_equalityreflexive).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA D E F U Q W) by (conclude lemma_equalangleshelper).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA U Q W D E F) by (conclude lemma_equalanglessymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA D E F U Q W) by (conclude lemma_equalangleshelper).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (LtA A B C U Q W) by (conclude lemma_angleorderrespectscongruence).
rename_H H;
let Tf:=fresh in
assert (Tf:exists H S T, (BetS S H T /\ Out Q U S /\ Out Q W T /\ CongA A B C U Q H)) by (conclude_def LtA );destruct Tf as [H[S[T]]];spliter.
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Out Q U P) by (conclude lemma_ray5).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (neq Q H) by (forward_using lemma_angledistinct).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (eq H H) by (conclude cn_equalityreflexive).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Out Q H H) by (conclude lemma_ray4).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA A B C P Q H) by (conclude lemma_equalangleshelper).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA D E F P Q T) by (conclude lemma_equalangleshelper).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (nCol P Q T) by (conclude lemma_equalanglesNC).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Triangle P Q T) by (conclude_def Triangle ).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (neq Q P) by (conclude lemma_ray2).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Out Q T W) by (conclude lemma_ray5).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (~ Col S Q T).
(* Goal: not (@Col Ax0 S Q T) *)
(* Goal: @LtA Ax0 A B C P Q R *)
 {
(* Goal: not (@Col Ax0 S Q T) *)
 intro.
(* Goal: False *)
 assert (Col Q U S) by (conclude lemma_rayimpliescollinear).
(* Goal: False *)
 assert (Col U Q S) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col Q P U) by (conclude lemma_rayimpliescollinear).
(* Goal: False *)
 assert (Col U Q P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq Q U) by (conclude lemma_raystrict).
(* Goal: False *)
 assert (neq U Q) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col Q S P) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col S Q P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq Q S) by (conclude lemma_raystrict).
(* Goal: False *)
 assert (neq S Q) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col Q T P) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col P Q T) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Triangle S Q T) by (conclude_def Triangle ).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Out Q S U) by (conclude lemma_ray5).
let Tf:=fresh in
assert (Tf:exists K, (Out Q H K /\ BetS U K W)) by (conclude lemma_crossbar);destruct Tf as [K];spliter.
(* Goal: @LtA Ax0 A B C P Q R *)
assert (BetS U K V) by (conclude lemma_3_6b).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (eq P P) by (conclude cn_equalityreflexive).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Out Q P P) by (conclude lemma_ray4).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA A B C P Q K) by (conclude lemma_equalangleshelper).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (LtA A B C P Q R) by (conclude_def LtA ).
(* Goal: @LtA Ax0 A B C P Q R *)
close.
Qed.

End Euclid.


