Require Export GeoCoq.Elements.OriginalProofs.proposition_03.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NCorder.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.
Require Export GeoCoq.Elements.OriginalProofs.lemma_ABCequalsCBA.
Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglestransitive.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_angleorderrespectscongruence : 
   forall A B C D E F P Q R, 
   LtA A B C D E F -> CongA P Q R D E F ->
   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) (_ : @CongA Ax0 P Q R D E F), @LtA Ax0 A B C P Q R *)
intros.
rename_H H;let Tf:=fresh in
assert (Tf:exists G H J, (BetS G H J /\ Out E D G /\ Out E F J /\ CongA A B C D E H)) by (conclude_def LtA );destruct Tf as [G[H[J]]];spliter.
(* Goal: @LtA Ax0 A B C P Q R *)
assert ((neq P Q /\ neq Q R /\ neq P R /\ neq D E /\ neq E F /\ neq D F)) by (forward_using lemma_angledistinct).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (neq Q P) by (conclude lemma_inequalitysymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert ((neq A B /\ neq B C /\ neq A C /\ neq D E /\ neq E H /\ neq D H)) by (forward_using lemma_angledistinct).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (neq E G) by (conclude lemma_raystrict).
let Tf:=fresh in
assert (Tf:exists U, (Out Q P U /\ Cong Q U E G)) by (conclude lemma_layoff);destruct Tf as [U];spliter.
(* Goal: @LtA Ax0 A B C P Q R *)
assert (neq E J) by (conclude lemma_raystrict).
let Tf:=fresh in
assert (Tf:exists V, (Out Q R V /\ Cong Q V E J)) by (conclude lemma_layoff);destruct Tf as [V];spliter.
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Cong G H G H) by (conclude cn_congruencereflexive).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Lt G H G J) by (conclude_def Lt ).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA D E F P Q R) by (conclude lemma_equalanglessymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA D E F U Q V) by (conclude lemma_equalangleshelper).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA U Q V D E F) by (conclude lemma_equalanglessymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA U Q V G E J) by (conclude lemma_equalangleshelper).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA G E J U Q V) by (conclude lemma_equalanglessymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Cong E G Q U) by (conclude lemma_congruencesymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Cong E J Q V) by (conclude lemma_congruencesymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert ((Cong G J U V /\ CongA E G J Q U V /\ CongA E J G Q V U)) by (conclude proposition_04).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Cong U V G J) by (conclude lemma_congruencesymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (neq G J) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists W, (BetS U W V /\ Cong U W G H)) by (conclude proposition_03);destruct Tf as [W];spliter.
(* 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 E H H) by (conclude lemma_ray4).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA A B C G E H) by (conclude lemma_equalangleshelper).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (nCol G E H) by (conclude lemma_equalanglesNC).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (nCol G H E) by (forward_using lemma_NCorder).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (neq U V) by (forward_using lemma_betweennotequal).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Out U V W) by (conclude lemma_ray4).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (eq Q Q) by (conclude cn_equalityreflexive).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (eq E E) by (conclude cn_equalityreflexive).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (nCol U Q V) by (conclude lemma_equalanglesNC).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (neq U Q) by (forward_using lemma_NCdistinct).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Out U Q Q) by (conclude lemma_ray4).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (~ eq G E).
(* Goal: not (@eq Ax0 Q W) *)
(* Goal: @LtA Ax0 A B C P Q R *)
 {
(* Goal: not (@eq Ax0 Q W) *)
 intro.
(* Goal: False *)
 assert (Col G H E) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Out G E E) by (conclude lemma_ray4).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA E G J Q U W) by (conclude lemma_equalangleshelper).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA Q U W E G J) by (conclude lemma_equalanglessymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Out G J H) by (conclude lemma_ray4).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA Q U W E G H) by (conclude lemma_equalangleshelper).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA E G H Q U W) by (conclude lemma_equalanglessymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (nCol Q U W) by (conclude lemma_equalanglesNC).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (nCol U W Q) by (forward_using lemma_NCorder).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (nCol H G E) by (forward_using lemma_NCorder).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (~ Col W U Q).
(* Goal: not (@eq Ax0 Q W) *)
(* Goal: @LtA Ax0 A B C P Q R *)
 {
(* Goal: not (@eq Ax0 Q W) *)
 intro.
(* Goal: False *)
 assert (Col U W Q) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Cong G H U W) by (conclude lemma_congruencesymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (Cong G E U Q) by (forward_using lemma_congruenceflip).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA E G H Q U W) by (conclude lemma_equalanglessymmetric).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA Q U W W U Q) by (conclude lemma_ABCequalsCBA).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA E G H W U Q) by (conclude lemma_equalanglestransitive).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA H G E E G H) by (conclude lemma_ABCequalsCBA).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA H G E W U Q) by (conclude lemma_equalanglestransitive).
(* Goal: @LtA Ax0 A B C P Q R *)
assert ((Cong H E W Q /\ CongA G H E U W Q /\ CongA G E H U Q W)) by (conclude proposition_04).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA A B C U 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 (~ eq Q W).
(* Goal: not (@eq Ax0 Q W) *)
(* Goal: @LtA Ax0 A B C P Q R *)
 {
(* Goal: not (@eq Ax0 Q W) *)
 intro.
(* Goal: False *)
 assert (Col Q U W) by (conclude_def Col ).
(* Goal: False *)
 assert (Col W U Q) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* 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 (Out Q U P) by (conclude lemma_ray5).
(* Goal: @LtA Ax0 A B C P Q R *)
assert (CongA A B C P Q W) 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.
