# Library GeoCoq.Elements.OriginalProofs.proposition_29

Require Export GeoCoq.Elements.OriginalProofs.proposition_31.

Require Export GeoCoq.Elements.OriginalProofs.lemma_crossbar2.

Require Export GeoCoq.Elements.OriginalProofs.lemma_supplementinequality.

Require Export GeoCoq.Elements.OriginalProofs.lemma_angletrichotomy2.

Require Export GeoCoq.Elements.OriginalProofs.lemma_supplementsymmetric.

Section Euclid.

Context `{Ax:euclidean_euclidean}.

Lemma proposition_29 :

∀ A B C D E G H,

Par A B C D → BetS A G B → BetS C H D → BetS E G H → TS A G H D →

CongA A G H G H D ∧ CongA E G B G H D ∧ RT B G H G H D.

Proof.

intros.

assert (Col C H D) by (conclude_def Col ).

assert (neq G H) by (forward_using lemma_betweennotequal).

assert (neq A B) by (forward_using lemma_betweennotequal).

assert (neq C D) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

assert (Tf:∃ R, (BetS A R D ∧ Col G H R ∧ nCol G H A)) by (conclude_def TS );destruct Tf as [R];spliter.

assert (TS D G H A) by (conclude lemma_oppositesidesymmetric).

assert (nCol G H D) by (conclude_def TS ).

assert (nCol D H G) by (forward_using lemma_NCorder).

assert (Col D H C) by (forward_using lemma_collinearorder).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (Col D H H) by (conclude_def Col ).

assert (neq C H) by (forward_using lemma_betweennotequal).

assert (nCol C H G) by (conclude lemma_NChelper).

assert (eq C C) by (conclude cn_equalityreflexive).

assert (Col C H C) by (conclude_def Col ).

assert (neq C D) by (forward_using lemma_betweennotequal).

assert (nCol C D G) by (conclude lemma_NChelper).

let Tf:=fresh in

assert (Tf:∃ P Q S, (BetS P G Q ∧ CongA Q G H G H C ∧ CongA Q G H C H G ∧ CongA H G Q C H G ∧ CongA P G H G H D ∧ CongA P G H D H G ∧ CongA H G P D H G ∧ Par P Q C D ∧ Cong P G H D ∧ Cong G Q C H ∧ Cong G S S H ∧ Cong P S S D ∧ Cong C S S Q ∧ BetS P S D ∧ BetS C S Q ∧ BetS G S H)) by (conclude proposition_31);destruct Tf as [P[Q[S]]];spliter.

assert (¬ Meet A B C D) by (conclude_def Par ).

assert (eq P P) by (conclude cn_equalityreflexive).

assert (neq P G) by (forward_using lemma_betweennotequal).

assert (neq G P) by (conclude lemma_inequalitysymmetric).

assert (Out G P P) by (conclude lemma_ray4).

assert (Col G S H) by (conclude_def Col ).

assert (Col G H S) by (forward_using lemma_collinearorder).

assert (CongA G H D P G H) by (conclude lemma_equalanglessymmetric).

assert (nCol P G H) by (conclude lemma_equalanglesNC).

assert (nCol G H P) by (forward_using lemma_NCorder).

assert (OS A P G H) by (conclude_def OS ).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (neq G H) by (forward_using lemma_betweennotequal).

assert (Out G H H) by (conclude lemma_ray4).

assert (¬ LtA H G A H G P).

{

intro.

let Tf:=fresh in

assert (Tf:∃ M, (BetS P M H ∧ Out G A M)) by (conclude lemma_crossbar2);destruct Tf as [M];spliter.

assert (Cong G S H S) by (forward_using lemma_congruenceflip).

assert (Cong S P S D) by (forward_using lemma_congruenceflip).

let Tf:=fresh in

assert (Tf:∃ K, (BetS G M K ∧ BetS D H K)) by (conclude postulate_Euclid5);destruct Tf as [K];spliter.

assert (Col G A M) by (conclude lemma_rayimpliescollinear).

assert (Col G M K) by (conclude_def Col ).

assert (Col M G A) by (forward_using lemma_collinearorder).

assert (Col M G K) by (forward_using lemma_collinearorder).

assert (neq G M) by (conclude lemma_raystrict).

assert (neq M G) by (conclude lemma_inequalitysymmetric).

assert (Col G A K) by (conclude lemma_collinear4).

assert (Col A G B) by (conclude_def Col ).

assert (Col A G K) by (forward_using lemma_collinearorder).

assert (Col G A B) by (forward_using lemma_collinearorder).

assert (Col G A K) by (forward_using lemma_collinearorder).

assert (neq A G) by (forward_using lemma_betweennotequal).

assert (neq G A) by (conclude lemma_inequalitysymmetric).

assert (Col A B K) by (conclude lemma_collinear4).

assert (Col H D K) by (conclude_def Col ).

assert (Col H D C) by (forward_using lemma_collinearorder).

assert (neq H D) by (forward_using lemma_betweennotequal).

assert (Col D K C) by (conclude lemma_collinear4).

assert (Col C D K) by (forward_using lemma_collinearorder).

assert (Meet A B C D) by (conclude_def Meet ).

contradict.

}

assert (¬ LtA H G P H G A).

{

intro.

assert (nCol P G H) by (forward_using lemma_NCorder).

assert (CongA P G H H G P) by (conclude lemma_ABCequalsCBA).

assert (LtA P G H H G A) by (conclude lemma_angleorderrespectscongruence2).

assert (¬ Col H G A).

{

intro.

assert (Col G H A) by (forward_using lemma_collinearorder).

contradict.

}

assert (CongA H G A A G H) by (conclude lemma_ABCequalsCBA).

assert (CongA A G H H G A) by (conclude lemma_equalanglessymmetric).

assert (LtA P G H A G H) by (conclude lemma_angleorderrespectscongruence).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (Out G H H) by (conclude lemma_ray4).

assert (Supp P G H H Q) by (conclude_def Supp ).

assert (BetS D H C) by (conclude axiom_betweennesssymmetry).

assert (eq G G) by (conclude cn_equalityreflexive).

assert (neq H G) by (conclude lemma_inequalitysymmetric).

assert (Out H G G) by (conclude lemma_ray4).

assert (Supp D H G G C) by (conclude_def Supp ).

assert (CongA G H D D H G) by (conclude lemma_ABCequalsCBA).

assert (CongA P G H D H G) by (conclude lemma_equalanglestransitive).

assert (CongA H G Q G H C) by (conclude lemma_supplements).

assert (Supp A G H H B) by (conclude_def Supp ).

assert (LtA H G B H G Q) by (conclude lemma_supplementinequality).

assert (BetS B G A) by (conclude axiom_betweennesssymmetry).

assert (eq G G) by (conclude cn_equalityreflexive).

assert (Col G H G) by (conclude_def Col ).

assert (¬ Col G H B).

{

intro.

assert (Col A G B) by (conclude_def Col ).

assert (Col B G A) by (forward_using lemma_collinearorder).

assert (Col B G H) by (forward_using lemma_collinearorder).

assert (neq G B) by (forward_using lemma_betweennotequal).

assert (neq B G) by (conclude lemma_inequalitysymmetric).

assert (Col G A H) by (conclude lemma_collinear4).

assert (Col H G A) by (forward_using lemma_collinearorder).

contradict.

}

assert (TS B G H A) by (conclude_def TS ).

assert (TS A G H B) by (conclude lemma_oppositesidesymmetric).

assert (OS A P G H) by (conclude_def OS ).

assert (OS P A G H) by (forward_using lemma_samesidesymmetric).

assert (TS P G H B) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ L, (BetS P L B ∧ Col G H L ∧ nCol G H P)) by (conclude_def TS );destruct Tf as [L];spliter.

assert (BetS B L P) by (conclude axiom_betweennesssymmetry).

assert (CongA G H C H G Q) by (conclude lemma_equalanglessymmetric).

assert (nCol H G Q) by (conclude lemma_equalanglesNC).

assert (¬ Col G H Q).

{

intro.

assert (Col H G Q) by (forward_using lemma_collinearorder).

contradict.

}

assert (BetS Q G P) by (conclude axiom_betweennesssymmetry).

assert (OS B Q G H) by (conclude_def OS ).

assert (eq Q Q) by (conclude cn_equalityreflexive).

assert (neq Q G) by (forward_using lemma_betweennotequal).

assert (neq G Q) by (conclude lemma_inequalitysymmetric).

assert (Out G Q Q) by (conclude lemma_ray4).

let Tf:=fresh in

assert (Tf:∃ M, (BetS Q M H ∧ Out G B M)) by (conclude lemma_crossbar2);destruct Tf as [M];spliter.

assert (Cong G S H S) by (forward_using lemma_congruenceflip).

assert (BetS Q S C) by (conclude axiom_betweennesssymmetry).

assert (Cong S Q C S) by (conclude lemma_congruencesymmetric).

assert (Cong S Q S C) by (forward_using lemma_congruenceflip).

assert (nCol G H C) by (forward_using lemma_NCorder).

let Tf:=fresh in

assert (Tf:∃ K, (BetS G M K ∧ BetS C H K)) by (conclude postulate_Euclid5);destruct Tf as [K];spliter.

assert (Col G B M) by (conclude lemma_rayimpliescollinear).

assert (Col G M K) by (conclude_def Col ).

assert (Col M G B) by (forward_using lemma_collinearorder).

assert (Col M G K) by (forward_using lemma_collinearorder).

assert (neq G M) by (conclude lemma_raystrict).

assert (neq M G) by (conclude lemma_inequalitysymmetric).

assert (Col G B K) by (conclude lemma_collinear4).

assert (Col B G A) by (conclude_def Col ).

assert (Col B G K) by (forward_using lemma_collinearorder).

assert (Col G B A) by (forward_using lemma_collinearorder).

assert (Col G B K) by (forward_using lemma_collinearorder).

assert (neq B G) by (forward_using lemma_betweennotequal).

assert (neq G B) by (conclude lemma_inequalitysymmetric).

assert (Col B A K) by (conclude lemma_collinear4).

assert (Col A B K) by (forward_using lemma_collinearorder).

assert (Col H C K) by (conclude_def Col ).

assert (Col H C D) by (forward_using lemma_collinearorder).

assert (neq H C) by (forward_using lemma_betweennotequal).

assert (Col C K D) by (conclude lemma_collinear4).

assert (Col C D K) by (forward_using lemma_collinearorder).

assert (Meet A B C D) by (conclude_def Meet ).

contradict.

}

assert (¬ Col H G P).

{

intro.

assert (Col G H P) by (forward_using lemma_collinearorder).

contradict.

}

assert (¬ Col H G A).

{

intro.

assert (Col G H A) by (forward_using lemma_collinearorder).

assert (nCol G H A) by (conclude_def TS ).

contradict.

}

assert (¬ ¬ CongA H G A H G P).

{

intro.

assert (LtA H G A H G P) by (conclude lemma_angletrichotomy2).

contradict.

}

assert (CongA H G P P G H) by (conclude lemma_ABCequalsCBA).

assert (CongA H G P G H D) by (conclude lemma_equalanglestransitive).

assert (CongA G H D D H G) by (conclude lemma_ABCequalsCBA).

assert (CongA H G P D H G) by (conclude lemma_equalanglestransitive).

assert (CongA H G A D H G) by (conclude lemma_equalanglestransitive).

assert (¬ Col A G H).

{

intro.

assert (Col G H A) by (forward_using lemma_collinearorder).

contradict.

}

assert (CongA A G H H G A) by (conclude lemma_ABCequalsCBA).

assert (CongA A G H D H G) by (conclude lemma_equalanglestransitive).

assert (nCol D H G) by (conclude lemma_equalanglesNC).

assert (CongA D H G G H D) by (conclude lemma_ABCequalsCBA).

assert (CongA A G H G H D) by (conclude lemma_equalanglestransitive).

assert (BetS H G E) by (conclude axiom_betweennesssymmetry).

assert (CongA A G H E G B) by (conclude proposition_15a).

assert (CongA E G B A G H) by (conclude lemma_equalanglessymmetric).

assert (CongA E G B G H D) by (conclude lemma_equalanglestransitive).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (Out G H H) by (conclude lemma_ray4).

assert (Supp A G H H B) by (conclude_def Supp ).

assert (¬ Col B G H).

{

intro.

assert (Col A G B) by (conclude_def Col ).

assert (Col B G A) by (forward_using lemma_collinearorder).

assert (neq G B) by (forward_using lemma_betweennotequal).

assert (neq B G) by (conclude lemma_inequalitysymmetric).

assert (Col G H A) by (conclude lemma_collinear4).

assert (Col A G H) by (forward_using lemma_collinearorder).

contradict.

}

assert (CongA B G H B G H) by (conclude lemma_equalanglesreflexive).

assert (CongA G H D A G H) by (conclude lemma_equalanglessymmetric).

assert (CongA A G H H G A) by (conclude lemma_ABCequalsCBA).

assert (CongA G H D H G A) by (conclude lemma_equalanglestransitive).

assert (Supp B G H H A) by (conclude lemma_supplementsymmetric).

assert (RT B G H G H D) by (conclude_def RT ).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_crossbar2.

Require Export GeoCoq.Elements.OriginalProofs.lemma_supplementinequality.

Require Export GeoCoq.Elements.OriginalProofs.lemma_angletrichotomy2.

Require Export GeoCoq.Elements.OriginalProofs.lemma_supplementsymmetric.

Section Euclid.

Context `{Ax:euclidean_euclidean}.

Lemma proposition_29 :

∀ A B C D E G H,

Par A B C D → BetS A G B → BetS C H D → BetS E G H → TS A G H D →

CongA A G H G H D ∧ CongA E G B G H D ∧ RT B G H G H D.

Proof.

intros.

assert (Col C H D) by (conclude_def Col ).

assert (neq G H) by (forward_using lemma_betweennotequal).

assert (neq A B) by (forward_using lemma_betweennotequal).

assert (neq C D) by (forward_using lemma_betweennotequal).

let Tf:=fresh in

assert (Tf:∃ R, (BetS A R D ∧ Col G H R ∧ nCol G H A)) by (conclude_def TS );destruct Tf as [R];spliter.

assert (TS D G H A) by (conclude lemma_oppositesidesymmetric).

assert (nCol G H D) by (conclude_def TS ).

assert (nCol D H G) by (forward_using lemma_NCorder).

assert (Col D H C) by (forward_using lemma_collinearorder).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (Col D H H) by (conclude_def Col ).

assert (neq C H) by (forward_using lemma_betweennotequal).

assert (nCol C H G) by (conclude lemma_NChelper).

assert (eq C C) by (conclude cn_equalityreflexive).

assert (Col C H C) by (conclude_def Col ).

assert (neq C D) by (forward_using lemma_betweennotequal).

assert (nCol C D G) by (conclude lemma_NChelper).

let Tf:=fresh in

assert (Tf:∃ P Q S, (BetS P G Q ∧ CongA Q G H G H C ∧ CongA Q G H C H G ∧ CongA H G Q C H G ∧ CongA P G H G H D ∧ CongA P G H D H G ∧ CongA H G P D H G ∧ Par P Q C D ∧ Cong P G H D ∧ Cong G Q C H ∧ Cong G S S H ∧ Cong P S S D ∧ Cong C S S Q ∧ BetS P S D ∧ BetS C S Q ∧ BetS G S H)) by (conclude proposition_31);destruct Tf as [P[Q[S]]];spliter.

assert (¬ Meet A B C D) by (conclude_def Par ).

assert (eq P P) by (conclude cn_equalityreflexive).

assert (neq P G) by (forward_using lemma_betweennotequal).

assert (neq G P) by (conclude lemma_inequalitysymmetric).

assert (Out G P P) by (conclude lemma_ray4).

assert (Col G S H) by (conclude_def Col ).

assert (Col G H S) by (forward_using lemma_collinearorder).

assert (CongA G H D P G H) by (conclude lemma_equalanglessymmetric).

assert (nCol P G H) by (conclude lemma_equalanglesNC).

assert (nCol G H P) by (forward_using lemma_NCorder).

assert (OS A P G H) by (conclude_def OS ).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (neq G H) by (forward_using lemma_betweennotequal).

assert (Out G H H) by (conclude lemma_ray4).

assert (¬ LtA H G A H G P).

{

intro.

let Tf:=fresh in

assert (Tf:∃ M, (BetS P M H ∧ Out G A M)) by (conclude lemma_crossbar2);destruct Tf as [M];spliter.

assert (Cong G S H S) by (forward_using lemma_congruenceflip).

assert (Cong S P S D) by (forward_using lemma_congruenceflip).

let Tf:=fresh in

assert (Tf:∃ K, (BetS G M K ∧ BetS D H K)) by (conclude postulate_Euclid5);destruct Tf as [K];spliter.

assert (Col G A M) by (conclude lemma_rayimpliescollinear).

assert (Col G M K) by (conclude_def Col ).

assert (Col M G A) by (forward_using lemma_collinearorder).

assert (Col M G K) by (forward_using lemma_collinearorder).

assert (neq G M) by (conclude lemma_raystrict).

assert (neq M G) by (conclude lemma_inequalitysymmetric).

assert (Col G A K) by (conclude lemma_collinear4).

assert (Col A G B) by (conclude_def Col ).

assert (Col A G K) by (forward_using lemma_collinearorder).

assert (Col G A B) by (forward_using lemma_collinearorder).

assert (Col G A K) by (forward_using lemma_collinearorder).

assert (neq A G) by (forward_using lemma_betweennotequal).

assert (neq G A) by (conclude lemma_inequalitysymmetric).

assert (Col A B K) by (conclude lemma_collinear4).

assert (Col H D K) by (conclude_def Col ).

assert (Col H D C) by (forward_using lemma_collinearorder).

assert (neq H D) by (forward_using lemma_betweennotequal).

assert (Col D K C) by (conclude lemma_collinear4).

assert (Col C D K) by (forward_using lemma_collinearorder).

assert (Meet A B C D) by (conclude_def Meet ).

contradict.

}

assert (¬ LtA H G P H G A).

{

intro.

assert (nCol P G H) by (forward_using lemma_NCorder).

assert (CongA P G H H G P) by (conclude lemma_ABCequalsCBA).

assert (LtA P G H H G A) by (conclude lemma_angleorderrespectscongruence2).

assert (¬ Col H G A).

{

intro.

assert (Col G H A) by (forward_using lemma_collinearorder).

contradict.

}

assert (CongA H G A A G H) by (conclude lemma_ABCequalsCBA).

assert (CongA A G H H G A) by (conclude lemma_equalanglessymmetric).

assert (LtA P G H A G H) by (conclude lemma_angleorderrespectscongruence).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (Out G H H) by (conclude lemma_ray4).

assert (Supp P G H H Q) by (conclude_def Supp ).

assert (BetS D H C) by (conclude axiom_betweennesssymmetry).

assert (eq G G) by (conclude cn_equalityreflexive).

assert (neq H G) by (conclude lemma_inequalitysymmetric).

assert (Out H G G) by (conclude lemma_ray4).

assert (Supp D H G G C) by (conclude_def Supp ).

assert (CongA G H D D H G) by (conclude lemma_ABCequalsCBA).

assert (CongA P G H D H G) by (conclude lemma_equalanglestransitive).

assert (CongA H G Q G H C) by (conclude lemma_supplements).

assert (Supp A G H H B) by (conclude_def Supp ).

assert (LtA H G B H G Q) by (conclude lemma_supplementinequality).

assert (BetS B G A) by (conclude axiom_betweennesssymmetry).

assert (eq G G) by (conclude cn_equalityreflexive).

assert (Col G H G) by (conclude_def Col ).

assert (¬ Col G H B).

{

intro.

assert (Col A G B) by (conclude_def Col ).

assert (Col B G A) by (forward_using lemma_collinearorder).

assert (Col B G H) by (forward_using lemma_collinearorder).

assert (neq G B) by (forward_using lemma_betweennotequal).

assert (neq B G) by (conclude lemma_inequalitysymmetric).

assert (Col G A H) by (conclude lemma_collinear4).

assert (Col H G A) by (forward_using lemma_collinearorder).

contradict.

}

assert (TS B G H A) by (conclude_def TS ).

assert (TS A G H B) by (conclude lemma_oppositesidesymmetric).

assert (OS A P G H) by (conclude_def OS ).

assert (OS P A G H) by (forward_using lemma_samesidesymmetric).

assert (TS P G H B) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ L, (BetS P L B ∧ Col G H L ∧ nCol G H P)) by (conclude_def TS );destruct Tf as [L];spliter.

assert (BetS B L P) by (conclude axiom_betweennesssymmetry).

assert (CongA G H C H G Q) by (conclude lemma_equalanglessymmetric).

assert (nCol H G Q) by (conclude lemma_equalanglesNC).

assert (¬ Col G H Q).

{

intro.

assert (Col H G Q) by (forward_using lemma_collinearorder).

contradict.

}

assert (BetS Q G P) by (conclude axiom_betweennesssymmetry).

assert (OS B Q G H) by (conclude_def OS ).

assert (eq Q Q) by (conclude cn_equalityreflexive).

assert (neq Q G) by (forward_using lemma_betweennotequal).

assert (neq G Q) by (conclude lemma_inequalitysymmetric).

assert (Out G Q Q) by (conclude lemma_ray4).

let Tf:=fresh in

assert (Tf:∃ M, (BetS Q M H ∧ Out G B M)) by (conclude lemma_crossbar2);destruct Tf as [M];spliter.

assert (Cong G S H S) by (forward_using lemma_congruenceflip).

assert (BetS Q S C) by (conclude axiom_betweennesssymmetry).

assert (Cong S Q C S) by (conclude lemma_congruencesymmetric).

assert (Cong S Q S C) by (forward_using lemma_congruenceflip).

assert (nCol G H C) by (forward_using lemma_NCorder).

let Tf:=fresh in

assert (Tf:∃ K, (BetS G M K ∧ BetS C H K)) by (conclude postulate_Euclid5);destruct Tf as [K];spliter.

assert (Col G B M) by (conclude lemma_rayimpliescollinear).

assert (Col G M K) by (conclude_def Col ).

assert (Col M G B) by (forward_using lemma_collinearorder).

assert (Col M G K) by (forward_using lemma_collinearorder).

assert (neq G M) by (conclude lemma_raystrict).

assert (neq M G) by (conclude lemma_inequalitysymmetric).

assert (Col G B K) by (conclude lemma_collinear4).

assert (Col B G A) by (conclude_def Col ).

assert (Col B G K) by (forward_using lemma_collinearorder).

assert (Col G B A) by (forward_using lemma_collinearorder).

assert (Col G B K) by (forward_using lemma_collinearorder).

assert (neq B G) by (forward_using lemma_betweennotequal).

assert (neq G B) by (conclude lemma_inequalitysymmetric).

assert (Col B A K) by (conclude lemma_collinear4).

assert (Col A B K) by (forward_using lemma_collinearorder).

assert (Col H C K) by (conclude_def Col ).

assert (Col H C D) by (forward_using lemma_collinearorder).

assert (neq H C) by (forward_using lemma_betweennotequal).

assert (Col C K D) by (conclude lemma_collinear4).

assert (Col C D K) by (forward_using lemma_collinearorder).

assert (Meet A B C D) by (conclude_def Meet ).

contradict.

}

assert (¬ Col H G P).

{

intro.

assert (Col G H P) by (forward_using lemma_collinearorder).

contradict.

}

assert (¬ Col H G A).

{

intro.

assert (Col G H A) by (forward_using lemma_collinearorder).

assert (nCol G H A) by (conclude_def TS ).

contradict.

}

assert (¬ ¬ CongA H G A H G P).

{

intro.

assert (LtA H G A H G P) by (conclude lemma_angletrichotomy2).

contradict.

}

assert (CongA H G P P G H) by (conclude lemma_ABCequalsCBA).

assert (CongA H G P G H D) by (conclude lemma_equalanglestransitive).

assert (CongA G H D D H G) by (conclude lemma_ABCequalsCBA).

assert (CongA H G P D H G) by (conclude lemma_equalanglestransitive).

assert (CongA H G A D H G) by (conclude lemma_equalanglestransitive).

assert (¬ Col A G H).

{

intro.

assert (Col G H A) by (forward_using lemma_collinearorder).

contradict.

}

assert (CongA A G H H G A) by (conclude lemma_ABCequalsCBA).

assert (CongA A G H D H G) by (conclude lemma_equalanglestransitive).

assert (nCol D H G) by (conclude lemma_equalanglesNC).

assert (CongA D H G G H D) by (conclude lemma_ABCequalsCBA).

assert (CongA A G H G H D) by (conclude lemma_equalanglestransitive).

assert (BetS H G E) by (conclude axiom_betweennesssymmetry).

assert (CongA A G H E G B) by (conclude proposition_15a).

assert (CongA E G B A G H) by (conclude lemma_equalanglessymmetric).

assert (CongA E G B G H D) by (conclude lemma_equalanglestransitive).

assert (eq H H) by (conclude cn_equalityreflexive).

assert (Out G H H) by (conclude lemma_ray4).

assert (Supp A G H H B) by (conclude_def Supp ).

assert (¬ Col B G H).

{

intro.

assert (Col A G B) by (conclude_def Col ).

assert (Col B G A) by (forward_using lemma_collinearorder).

assert (neq G B) by (forward_using lemma_betweennotequal).

assert (neq B G) by (conclude lemma_inequalitysymmetric).

assert (Col G H A) by (conclude lemma_collinear4).

assert (Col A G H) by (forward_using lemma_collinearorder).

contradict.

}

assert (CongA B G H B G H) by (conclude lemma_equalanglesreflexive).

assert (CongA G H D A G H) by (conclude lemma_equalanglessymmetric).

assert (CongA A G H H G A) by (conclude lemma_ABCequalsCBA).

assert (CongA G H D H G A) by (conclude lemma_equalanglestransitive).

assert (Supp B G H H A) by (conclude lemma_supplementsymmetric).

assert (RT B G H G H D) by (conclude_def RT ).

close.

Qed.

End Euclid.