# Library GeoCoq.Elements.OriginalProofs.proposition_43

Require Export GeoCoq.Elements.OriginalProofs.lemma_PGflip.

Require Export GeoCoq.Elements.OriginalProofs.proposition_34.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_43 :

∀ 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.

intros.

assert (PG B A D C) by (conclude lemma_PGflip).

assert (Cong_3 A B C C D A) by (conclude proposition_34).

assert (ET A B C C D A) by (conclude axiom_congruentequal).

assert (Cong_3 A E K K H A) by (conclude proposition_34).

assert (ET A E K K H A) by (conclude axiom_congruentequal).

assert (Cong_3 K G C C F K) by (conclude proposition_34).

assert (ET K G C C F K) by (conclude axiom_congruentequal).

assert (ET K G C K C F) by (forward_using axiom_ETpermutation).

assert (ET K C F K G C) by (conclude axiom_ETsymmetric).

assert (ET K C F K C G) by (forward_using axiom_ETpermutation).

assert (ET K C G K C F) by (conclude axiom_ETsymmetric).

assert (ET A B C A C D) by (forward_using axiom_ETpermutation).

assert (ET A C D A B C) by (conclude axiom_ETsymmetric).

assert (ET A C D A C B) by (forward_using axiom_ETpermutation).

assert (ET A C B A C D) by (conclude axiom_ETsymmetric).

assert (EF A K G B A K F D) by (conclude axiom_cutoff1).

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

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

assert (ET A E K H A K) by (forward_using axiom_ETpermutation).

assert (ET H A K A E K) by (conclude axiom_ETsymmetric).

assert (ET H A K E A K) by (forward_using axiom_ETpermutation).

assert (ET E A K H A K) by (conclude axiom_ETsymmetric).

assert (EF A K G B F D A K) by (forward_using axiom_EFpermutation).

assert (EF F D A K A K G B) by (conclude axiom_EFsymmetric).

assert (EF F D A K G B A K) by (forward_using axiom_EFpermutation).

assert (EF G B A K F D A K) by (conclude axiom_EFsymmetric).

assert (EF G B E K F D H K) by (conclude axiom_cutoff2).

assert (EF G B E K D F K H) by (forward_using axiom_EFpermutation).

assert (EF D F K H G B E K) by (conclude axiom_EFsymmetric).

assert (EF D F K H K G B E) by (forward_using axiom_EFpermutation).

assert (EF K G B E D F K H) by (conclude axiom_EFsymmetric).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.proposition_34.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_43 :

∀ 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.

intros.

assert (PG B A D C) by (conclude lemma_PGflip).

assert (Cong_3 A B C C D A) by (conclude proposition_34).

assert (ET A B C C D A) by (conclude axiom_congruentequal).

assert (Cong_3 A E K K H A) by (conclude proposition_34).

assert (ET A E K K H A) by (conclude axiom_congruentequal).

assert (Cong_3 K G C C F K) by (conclude proposition_34).

assert (ET K G C C F K) by (conclude axiom_congruentequal).

assert (ET K G C K C F) by (forward_using axiom_ETpermutation).

assert (ET K C F K G C) by (conclude axiom_ETsymmetric).

assert (ET K C F K C G) by (forward_using axiom_ETpermutation).

assert (ET K C G K C F) by (conclude axiom_ETsymmetric).

assert (ET A B C A C D) by (forward_using axiom_ETpermutation).

assert (ET A C D A B C) by (conclude axiom_ETsymmetric).

assert (ET A C D A C B) by (forward_using axiom_ETpermutation).

assert (ET A C B A C D) by (conclude axiom_ETsymmetric).

assert (EF A K G B A K F D) by (conclude axiom_cutoff1).

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

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

assert (ET A E K H A K) by (forward_using axiom_ETpermutation).

assert (ET H A K A E K) by (conclude axiom_ETsymmetric).

assert (ET H A K E A K) by (forward_using axiom_ETpermutation).

assert (ET E A K H A K) by (conclude axiom_ETsymmetric).

assert (EF A K G B F D A K) by (forward_using axiom_EFpermutation).

assert (EF F D A K A K G B) by (conclude axiom_EFsymmetric).

assert (EF F D A K G B A K) by (forward_using axiom_EFpermutation).

assert (EF G B A K F D A K) by (conclude axiom_EFsymmetric).

assert (EF G B E K F D H K) by (conclude axiom_cutoff2).

assert (EF G B E K D F K H) by (forward_using axiom_EFpermutation).

assert (EF D F K H G B E K) by (conclude axiom_EFsymmetric).

assert (EF D F K H K G B E) by (forward_using axiom_EFpermutation).

assert (EF K G B E D F K H) by (conclude axiom_EFsymmetric).

close.

Qed.

End Euclid.