Require Export GeoCoq.Elements.OriginalProofs.lemma_paralleldef2B.
Require Export GeoCoq.Elements.OriginalProofs.lemma_samesideflip.
Require Export GeoCoq.Elements.OriginalProofs.proposition_29C.
Require Export GeoCoq.Elements.OriginalProofs.lemma_supplements2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_samesidecollinear.
Require Export GeoCoq.Elements.OriginalProofs.lemma_samesidetransitive.
Require Export GeoCoq.Elements.OriginalProofs.proposition_28D.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_43B : 
   forall A B C D E F G H K, 
   PG A B C D -> BetS A H D -> BetS A E B -> BetS D F C -> BetS B G C -> PG E A H K -> PG G K F C ->
   PG E K G B.
Proof.
(* Goal: forall (A B C D E F G H K : @Point Ax0) (_ : @PG Ax0 A B C D) (_ : @BetS Ax0 A H D) (_ : @BetS Ax0 A E B) (_ : @BetS Ax0 D F C) (_ : @BetS Ax0 B G C) (_ : @PG Ax0 E A H K) (_ : @PG Ax0 G K F C), @PG Ax0 E K G B *)
intros.
(* Goal: @PG Ax0 E K G B *)
assert (Par A D B C) by (conclude_def PG ).
(* Goal: @PG Ax0 E K G B *)
assert (Par A B C D) by (conclude_def PG ).
(* Goal: @PG Ax0 E K G B *)
assert (Par E A H K) by (conclude_def PG ).
(* Goal: @PG Ax0 E K G B *)
assert (Par E K A H) by (conclude_def PG ).
(* Goal: @PG Ax0 E K G B *)
assert (Par G K F C) by (conclude_def PG ).
(* Goal: @PG Ax0 E K G B *)
assert (Par F C G K) by (conclude lemma_parallelsymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (Par C F G K) by (forward_using lemma_parallelflip).
(* Goal: @PG Ax0 E K G B *)
assert (Par G C K F) by (conclude_def PG ).
(* Goal: @PG Ax0 E K G B *)
assert (Par B C A D) by (conclude lemma_parallelsymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (Par C D A B) by (conclude lemma_parallelsymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (Par A H E K) by (conclude lemma_parallelsymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (TP A B C D) by (conclude lemma_paralleldef2B).
(* Goal: @PG Ax0 E K G B *)
assert (TP E A H K) by (conclude lemma_paralleldef2B).
(* Goal: @PG Ax0 E K G B *)
assert (TP G C K F) by (conclude lemma_paralleldef2B).
(* Goal: @PG Ax0 E K G B *)
assert (TP B C A D) by (conclude lemma_paralleldef2B).
(* Goal: @PG Ax0 E K G B *)
assert (OS A D B C) by (conclude_def TP ).
(* Goal: @PG Ax0 E K G B *)
assert (OS A D C B) by (conclude lemma_samesideflip).
(* Goal: @PG Ax0 E K G B *)
assert (OS D A C B) by (forward_using lemma_samesidesymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (OS C D A B) by (conclude_def TP ).
(* Goal: @PG Ax0 E K G B *)
assert (OS H K E A) by (conclude_def TP ).
(* Goal: @PG Ax0 E K G B *)
assert (OS K F G C) by (conclude_def TP ).
(* Goal: @PG Ax0 E K G B *)
assert (neq A E) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 E K G B *)
assert (neq A H) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 E K G B *)
assert (neq B G) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 E K G B *)
assert (neq A B) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 E K G B *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists e, (BetS B A e /\ Cong A e B A)) by (conclude lemma_extension);destruct Tf as [e];spliter.
(* Goal: @PG Ax0 E K G B *)
assert (BetS e A B) by (conclude axiom_betweennesssymmetry).
(* Goal: @PG Ax0 E K G B *)
assert (OS D C A B) by (forward_using lemma_samesidesymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (RT D A B A B C) by (conclude proposition_29C).
(* Goal: @PG Ax0 E K G B *)
assert (BetS B E A) by (conclude axiom_betweennesssymmetry).
(* Goal: @PG Ax0 E K G B *)
assert (BetS E A e) by (conclude lemma_3_6a).
(* Goal: @PG Ax0 E K G B *)
assert (BetS e A E) by (conclude axiom_betweennesssymmetry).
(* Goal: @PG Ax0 E K G B *)
assert (OS H K A E) by (forward_using lemma_samesidesymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (RT H A E A E K) by (conclude proposition_29C).
(* Goal: @PG Ax0 E K G B *)
assert (Out A E B) by (conclude lemma_ray4).
(* Goal: @PG Ax0 E K G B *)
assert (Out A H D) by (conclude lemma_ray4).
(* Goal: @PG Ax0 E K G B *)
assert (nCol A H E) by (forward_using lemma_parallelNC).
(* Goal: @PG Ax0 E K G B *)
assert (nCol E A H) by (forward_using lemma_NCorder).
(* Goal: @PG Ax0 E K G B *)
assert (CongA E A H E A H) by (conclude lemma_equalanglesreflexive).
(* Goal: @PG Ax0 E K G B *)
assert (CongA E A H B A D) by (conclude lemma_equalangleshelper).
(* Goal: @PG Ax0 E K G B *)
assert (CongA H A E D A B) by (conclude lemma_equalanglesflip).
assert (CongA A E K A B C)  by (apply (lemma_supplements2 H A E A B C D A B A E K);eauto).
(* Goal: @PG Ax0 E K G B *)
assert (OS C D B A) by (conclude lemma_samesideflip).
(* Goal: @PG Ax0 E K G B *)
assert (Col A E B) by (conclude_def Col ).
(* Goal: @PG Ax0 E K G B *)
assert (Col B A E) by (forward_using lemma_collinearorder).
(* Goal: @PG Ax0 E K G B *)
assert (neq E B) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 E K G B *)
assert (neq B E) by (conclude lemma_inequalitysymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (OS C D B E) by (conclude lemma_samesidecollinear).
(* Goal: @PG Ax0 E K G B *)
assert (Out A H D) by (conclude lemma_ray4).
(* Goal: @PG Ax0 E K G B *)
assert (Out A D H) by (conclude lemma_ray5).
(* Goal: @PG Ax0 E K G B *)
assert (OS C H B E) by (conclude lemma_sameside2).
(* Goal: @PG Ax0 E K G B *)
assert (Col E A B) by (forward_using lemma_collinearorder).
(* Goal: @PG Ax0 E K G B *)
assert (OS H K E B) by (conclude lemma_samesidecollinear).
(* Goal: @PG Ax0 E K G B *)
assert (OS H K B E) by (conclude lemma_samesideflip).
(* Goal: @PG Ax0 E K G B *)
assert (OS C K B E) by (conclude lemma_samesidetransitive).
(* Goal: @PG Ax0 E K G B *)
assert (OS K C B E) by (forward_using lemma_samesidesymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (Out B G C) by (conclude lemma_ray4).
(* Goal: @PG Ax0 E K G B *)
assert (Out B C G) by (conclude lemma_ray5).
(* Goal: @PG Ax0 E K G B *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 E K G B *)
assert (Col B B E) by (conclude_def Col ).
(* Goal: @PG Ax0 E K G B *)
assert (OS K G B E) by (conclude lemma_sameside2).
(* Goal: @PG Ax0 E K G B *)
assert (OS K G E B) by (conclude lemma_samesideflip).
(* Goal: @PG Ax0 E K G B *)
assert (Out B E A) by (conclude lemma_ray4).
(* Goal: @PG Ax0 E K G B *)
assert (Out B A E) by (conclude lemma_ray5).
(* Goal: @PG Ax0 E K G B *)
assert (CongA A E K E B G) by (conclude lemma_equalangleshelper).
(* Goal: @PG Ax0 E K G B *)
assert (Par E K B G) by (conclude proposition_28D).
(* Goal: @PG Ax0 E K G B *)
assert (Par E K G B) by (forward_using lemma_parallelflip).
(* Goal: @PG Ax0 E K G B *)
assert (neq B C) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists c, (BetS B C c /\ Cong C c B C)) by (conclude lemma_extension);destruct Tf as [c];spliter.
(* Goal: @PG Ax0 E K G B *)
assert (BetS c C B) by (conclude axiom_betweennesssymmetry).
(* Goal: @PG Ax0 E K G B *)
assert (Par C D B A) by (forward_using lemma_parallelflip).
(* Goal: @PG Ax0 E K G B *)
assert (RT D C B C B A) by (conclude proposition_29C).
(* Goal: @PG Ax0 E K G B *)
assert (OS K F C G) by (conclude lemma_samesideflip).
(* Goal: @PG Ax0 E K G B *)
assert (OS F K C G) by (forward_using lemma_samesidesymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (BetS C G B) by (conclude axiom_betweennesssymmetry).
(* Goal: @PG Ax0 E K G B *)
assert (BetS c C G) by (conclude axiom_innertransitivity).
(* Goal: @PG Ax0 E K G B *)
assert (RT F C G C G K) by (conclude proposition_29C).
(* Goal: @PG Ax0 E K G B *)
assert (nCol D B C) by (forward_using lemma_parallelNC).
(* Goal: @PG Ax0 E K G B *)
assert (nCol D C B) by (forward_using lemma_NCorder).
(* Goal: @PG Ax0 E K G B *)
assert (CongA D C B D C B) by (conclude lemma_equalanglesreflexive).
(* Goal: @PG Ax0 E K G B *)
assert (BetS C F D) by (conclude axiom_betweennesssymmetry).
(* Goal: @PG Ax0 E K G B *)
assert (neq C F) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 E K G B *)
assert (Out C F D) by (conclude lemma_ray4).
(* Goal: @PG Ax0 E K G B *)
assert (Out C D F) by (conclude lemma_ray5).
(* Goal: @PG Ax0 E K G B *)
assert (BetS C G B) by (conclude axiom_betweennesssymmetry).
(* Goal: @PG Ax0 E K G B *)
assert (neq C G) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 E K G B *)
assert (Out C G B) by (conclude lemma_ray4).
(* Goal: @PG Ax0 E K G B *)
assert (Out C B G) by (conclude lemma_ray5).
(* Goal: @PG Ax0 E K G B *)
assert (CongA D C B F C G) by (conclude lemma_equalangleshelper).
(* Goal: @PG Ax0 E K G B *)
assert (CongA C B A C G K) by (conclude (lemma_supplements2 D C B C G K F C G C B A)).
(* Goal: @PG Ax0 E K G B *)
assert (CongA C G K C B A) by (conclude lemma_equalanglessymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 E K G B *)
assert (Out B A A) by (conclude lemma_ray4).
(* Goal: @PG Ax0 E K G B *)
assert (neq B G) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 E K G B *)
assert (Out B G C) by (conclude lemma_ray4).
(* Goal: @PG Ax0 E K G B *)
assert (Out B C G) by (conclude lemma_ray5).
(* Goal: @PG Ax0 E K G B *)
assert (CongA C G K G B A) by (conclude lemma_equalangleshelper).
(* Goal: @PG Ax0 E K G B *)
assert (Col B G C) by (conclude_def Col ).
(* Goal: @PG Ax0 E K G B *)
assert (Col C B G) by (forward_using lemma_collinearorder).
(* Goal: @PG Ax0 E K G B *)
assert (BetS C F D) by (conclude axiom_betweennesssymmetry).
(* Goal: @PG Ax0 E K G B *)
assert (neq C F) by (forward_using lemma_betweennotequal).
(* Goal: @PG Ax0 E K G B *)
assert (Out C F D) by (conclude lemma_ray4).
(* Goal: @PG Ax0 E K G B *)
assert (Out C D F) by (conclude lemma_ray5).
(* Goal: @PG Ax0 E K G B *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: @PG Ax0 E K G B *)
assert (Col B C C) by (conclude_def Col ).
(* Goal: @PG Ax0 E K G B *)
assert (OS A F B C) by (conclude lemma_sameside2).
(* Goal: @PG Ax0 E K G B *)
assert (TP G C K F) by (conclude lemma_paralleldef2B).
(* Goal: @PG Ax0 E K G B *)
assert (OS K F G C) by (conclude_def TP ).
(* Goal: @PG Ax0 E K G B *)
assert (Col C G B) by (forward_using lemma_collinearorder).
(* Goal: @PG Ax0 E K G B *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (OS K F C G) by (conclude lemma_samesideflip).
(* Goal: @PG Ax0 E K G B *)
assert (OS K F C B) by (conclude lemma_samesidecollinear).
(* Goal: @PG Ax0 E K G B *)
assert (OS K F B C) by (conclude lemma_samesideflip).
(* Goal: @PG Ax0 E K G B *)
assert (OS F K B C) by (forward_using lemma_samesidesymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (OS A K B C) by (conclude lemma_samesidetransitive).
(* Goal: @PG Ax0 E K G B *)
assert (OS K A B C) by (forward_using lemma_samesidesymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (Col B C G) by (forward_using lemma_collinearorder).
(* Goal: @PG Ax0 E K G B *)
assert (OS K A B G) by (conclude lemma_samesidecollinear).
(* Goal: @PG Ax0 E K G B *)
assert (OS K A G B) by (conclude lemma_samesideflip).
(* Goal: @PG Ax0 E K G B *)
assert (Par G K B A) by (conclude proposition_28D).
(* Goal: @PG Ax0 E K G B *)
assert (Par G K A B) by (forward_using lemma_parallelflip).
(* Goal: @PG Ax0 E K G B *)
assert (Col A B E) by (forward_using lemma_collinearorder).
(* Goal: @PG Ax0 E K G B *)
assert (Par G K E B) by (conclude lemma_collinearparallel).
(* Goal: @PG Ax0 E K G B *)
assert (Par E B G K) by (conclude lemma_parallelsymmetric).
(* Goal: @PG Ax0 E K G B *)
assert (Par E B K G) by (forward_using lemma_parallelflip).
(* Goal: @PG Ax0 E K G B *)
assert (PG E K G B) by (conclude_def PG ).
(* Goal: @PG Ax0 E K G B *)
close.
Qed.

End Euclid.


