Require Export GeoCoq.Elements.OriginalProofs.lemma_PGflip.
Require Export GeoCoq.Elements.OriginalProofs.proposition_34.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_43 : 
   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 -> BetS A K C -> PG E A H K -> PG G K F C ->
   EF K G B E D F K H.
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) (_ : @BetS Ax0 A K C) (_ : @PG Ax0 E A H K) (_ : @PG Ax0 G K F C), @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
intros.
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (PG B A D C) by (conclude lemma_PGflip).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (Cong_3 A B C C D A) by (conclude proposition_34).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET A B C C D A) by (conclude axiom_congruentequal).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (Cong_3 A E K K H A) by (conclude proposition_34).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET A E K K H A) by (conclude axiom_congruentequal).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (Cong_3 K G C C F K) by (conclude proposition_34).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET K G C C F K) by (conclude axiom_congruentequal).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET K G C K C F) by (forward_using axiom_ETpermutation).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET K C F K G C) by (conclude axiom_ETsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET K C F K C G) by (forward_using axiom_ETpermutation).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET K C G K C F) by (conclude axiom_ETsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET A B C A C D) by (forward_using axiom_ETpermutation).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET A C D A B C) by (conclude axiom_ETsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET A C D A C B) by (forward_using axiom_ETpermutation).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET A C B A C D) by (conclude axiom_ETsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (EF A K G B A K F D) by (conclude axiom_cutoff1).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (BetS B E A) by (conclude axiom_betweennesssymmetry).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (BetS D H A) by (conclude axiom_betweennesssymmetry).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET A E K H A K) by (forward_using axiom_ETpermutation).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET H A K A E K) by (conclude axiom_ETsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET H A K E A K) by (forward_using axiom_ETpermutation).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (ET E A K H A K) by (conclude axiom_ETsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (EF A K G B F D A K) by (forward_using axiom_EFpermutation).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (EF F D A K A K G B) by (conclude axiom_EFsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (EF F D A K G B A K) by (forward_using axiom_EFpermutation).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (EF G B A K F D A K) by (conclude axiom_EFsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (EF G B E K F D H K) by (conclude axiom_cutoff2).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (EF G B E K D F K H) by (forward_using axiom_EFpermutation).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (EF D F K H G B E K) by (conclude axiom_EFsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (EF D F K H K G B E) by (forward_using axiom_EFpermutation).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
assert (EF K G B E D F K H) by (conclude axiom_EFsymmetric).
(* Goal: @EF Ax0 Ax1 Ax2 Ax K G B E D F K H *)
close.
Qed.

End Euclid.


