Library GeoCoq.Elements.OriginalProofs.proposition_43B
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 :
∀ 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 →
PG E K G B.
Proof.
intros.
assert (Par A D B C) by (conclude_def PG ).
assert (Par A B C D) by (conclude_def PG ).
assert (Par E A H K) by (conclude_def PG ).
assert (Par E K A H) by (conclude_def PG ).
assert (Par G K F C) by (conclude_def PG ).
assert (Par F C G K) by (conclude lemma_parallelsymmetric).
assert (Par C F G K) by (forward_using lemma_parallelflip).
assert (Par G C K F) by (conclude_def PG ).
assert (Par B C A D) by (conclude lemma_parallelsymmetric).
assert (Par C D A B) by (conclude lemma_parallelsymmetric).
assert (Par H K E A) by (conclude lemma_parallelsymmetric).
assert (Par A H E K) by (conclude lemma_parallelsymmetric).
assert (Par F C G K) by (conclude lemma_parallelsymmetric).
assert (Par K F G C) by (conclude lemma_parallelsymmetric).
assert (TP A D B C) by (conclude lemma_paralleldef2B).
assert (TP A B C D) by (conclude lemma_paralleldef2B).
assert (TP E A H K) by (conclude lemma_paralleldef2B).
assert (TP E K A H) by (conclude lemma_paralleldef2B).
assert (TP G K F C) by (conclude lemma_paralleldef2B).
assert (TP G C K F) by (conclude lemma_paralleldef2B).
assert (TP B C A D) by (conclude lemma_paralleldef2B).
assert (TP C D A B) by (conclude lemma_paralleldef2B).
assert (TP H K E A) by (conclude lemma_paralleldef2B).
assert (TP A H E K) by (conclude lemma_paralleldef2B).
assert (TP F C G K) by (conclude lemma_paralleldef2B).
assert (TP K F G C) by (conclude lemma_paralleldef2B).
assert (OS A D B C) by (conclude_def TP ).
assert (OS A D C B) by (conclude lemma_samesideflip).
assert (OS D A C B) by (forward_using lemma_samesidesymmetric).
assert (OS A B C D) by (conclude_def TP ).
assert (OS E A H K) by (conclude_def TP ).
assert (OS E K A H) by (conclude_def TP ).
assert (OS G K F C) by (conclude_def TP ).
assert (OS G C K F) by (conclude_def TP ).
assert (OS B C A D) by (conclude_def TP ).
assert (OS C D A B) by (conclude_def TP ).
assert (OS H K E A) by (conclude_def TP ).
assert (OS A H E K) by (conclude_def TP ).
assert (OS F C G K) by (conclude_def TP ).
assert (OS K F G C) by (conclude_def TP ).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (neq E A) by (conclude lemma_inequalitysymmetric).
assert (neq D F) by (forward_using lemma_betweennotequal).
assert (neq A H) by (forward_using lemma_betweennotequal).
assert (neq B G) by (forward_using lemma_betweennotequal).
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ e, (BetS B A e ∧ Cong A e B A)) by (conclude postulate_extension);destruct Tf as [e];spliter.
assert (BetS e A B) by (conclude axiom_betweennesssymmetry).
assert (OS D C A B) by (forward_using lemma_samesidesymmetric).
assert (RT D A B A B C) by (conclude proposition_29C).
assert (BetS B E A) by (conclude axiom_betweennesssymmetry).
assert (BetS E A e) by (conclude lemma_3_6a).
assert (BetS e A E) by (conclude axiom_betweennesssymmetry).
assert (OS H K A E) by (forward_using lemma_samesidesymmetric).
assert (RT H A E A E K) by (conclude proposition_29C).
assert (Out A E B) by (conclude lemma_ray4).
assert (Out A H D) by (conclude lemma_ray4).
assert (nCol A H E) by (forward_using lemma_parallelNC).
assert (nCol E A H) by (forward_using lemma_NCorder).
assert (CongA E A H E A H) by (conclude lemma_equalanglesreflexive).
assert (CongA E A H B A D) by (conclude lemma_equalangleshelper).
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).
assert (Col D F C) by (conclude_def Col ).
assert (Col D C F) by (forward_using lemma_collinearorder).
assert (OS C D B A) by (conclude lemma_samesideflip).
assert (Col A E B) by (conclude_def Col ).
assert (Col B A E) by (forward_using lemma_collinearorder).
assert (neq E B) by (forward_using lemma_betweennotequal).
assert (neq B E) by (conclude lemma_inequalitysymmetric).
assert (OS C D B E) by (conclude lemma_samesidecollinear).
assert (Out A H D) by (conclude lemma_ray4).
assert (Out A D H) by (conclude lemma_ray5).
assert (OS C H B E) by (conclude lemma_sameside2).
assert (Col E A B) by (forward_using lemma_collinearorder).
assert (OS H K E B) by (conclude lemma_samesidecollinear).
assert (OS H K B E) by (conclude lemma_samesideflip).
assert (OS C K B E) by (conclude lemma_samesidetransitive).
assert (OS K C B E) by (forward_using lemma_samesidesymmetric).
assert (Out B G C) by (conclude lemma_ray4).
assert (Out B C G) by (conclude lemma_ray5).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col B B E) by (conclude_def Col ).
assert (OS K G B E) by (conclude lemma_sameside2).
assert (OS K G E B) by (conclude lemma_samesideflip).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Out B E A) by (conclude lemma_ray4).
assert (Out B A E) by (conclude lemma_ray5).
assert (CongA A E K E B G) by (conclude lemma_equalangleshelper).
assert (Par E K B G) by (conclude proposition_28D).
assert (Par E K G B) by (forward_using lemma_parallelflip).
assert (neq B C) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:∃ c, (BetS B C c ∧ Cong C c B C)) by (conclude postulate_extension);destruct Tf as [c];spliter.
assert (BetS c C B) by (conclude axiom_betweennesssymmetry).
assert (Par C D B A) by (forward_using lemma_parallelflip).
assert (RT D C B C B A) by (conclude proposition_29C).
assert (OS K F C G) by (conclude lemma_samesideflip).
assert (OS F K C G) by (forward_using lemma_samesidesymmetric).
assert (BetS C G B) by (conclude axiom_betweennesssymmetry).
assert (BetS c C G) by (conclude axiom_innertransitivity).
assert (RT F C G C G K) by (conclude proposition_29C).
assert (nCol D B C) by (forward_using lemma_parallelNC).
assert (nCol D C B) by (forward_using lemma_NCorder).
assert (CongA D C B D C B) by (conclude lemma_equalanglesreflexive).
assert (BetS C F D) by (conclude axiom_betweennesssymmetry).
assert (neq C F) by (forward_using lemma_betweennotequal).
assert (Out C F D) by (conclude lemma_ray4).
assert (Out C D F) by (conclude lemma_ray5).
assert (BetS C G B) by (conclude axiom_betweennesssymmetry).
assert (neq C G) by (forward_using lemma_betweennotequal).
assert (Out C G B) by (conclude lemma_ray4).
assert (Out C B G) by (conclude lemma_ray5).
assert (CongA D C B F C G) by (conclude lemma_equalangleshelper).
assert (CongA C B A C G K) by (conclude (lemma_supplements2 D C B C G K F C G C B A)).
assert (CongA C G K C B A) by (conclude lemma_equalanglessymmetric).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Out B A A) by (conclude lemma_ray4).
assert (neq B G) by (forward_using lemma_betweennotequal).
assert (Out B G C) by (conclude lemma_ray4).
assert (Out B C G) by (conclude lemma_ray5).
assert (CongA C G K G B A) by (conclude lemma_equalangleshelper).
assert (Col B G C) by (conclude_def Col ).
assert (Col C B G) by (forward_using lemma_collinearorder).
assert (neq B G) by (forward_using lemma_betweennotequal).
assert (neq G B) by (conclude lemma_inequalitysymmetric).
assert (Par A D C B) by (forward_using lemma_parallelflip).
assert (Par A D G B) by (conclude lemma_collinearparallel).
assert (Par A D B G) by (forward_using lemma_parallelflip).
assert (Par B G A D) by (conclude lemma_parallelsymmetric).
assert (Par G B D A) by (forward_using lemma_parallelflip).
assert (Col A H D) by (conclude_def Col ).
assert (Col D A H) by (forward_using lemma_collinearorder).
assert (neq H A) by (conclude lemma_inequalitysymmetric).
assert (Par G B H A) by (conclude lemma_collinearparallel).
assert (TP G B H A) by (conclude lemma_paralleldef2B).
assert (OS H A G B) by (conclude_def TP ).
assert (BetS C F D) by (conclude axiom_betweennesssymmetry).
assert (neq C F) by (forward_using lemma_betweennotequal).
assert (Out C F D) by (conclude lemma_ray4).
assert (Out C D F) by (conclude lemma_ray5).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col B C C) by (conclude_def Col ).
assert (OS A F B C) by (conclude lemma_sameside2).
assert (TP G C K F) by (conclude lemma_paralleldef2B).
assert (OS K F G C) by (conclude_def TP ).
assert (Col B G C) by (conclude_def Col ).
assert (Col C G B) by (forward_using lemma_collinearorder).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (OS K F C G) by (conclude lemma_samesideflip).
assert (OS K F C B) by (conclude lemma_samesidecollinear).
assert (OS K F B C) by (conclude lemma_samesideflip).
assert (OS F K B C) by (forward_using lemma_samesidesymmetric).
assert (OS A K B C) by (conclude lemma_samesidetransitive).
assert (OS K A B C) by (forward_using lemma_samesidesymmetric).
assert (Col B C G) by (forward_using lemma_collinearorder).
assert (OS K A B G) by (conclude lemma_samesidecollinear).
assert (OS K A G B) by (conclude lemma_samesideflip).
assert (Par G K B A) by (conclude proposition_28D).
assert (Par G K A B) by (forward_using lemma_parallelflip).
assert (Col A E B) by (conclude_def Col ).
assert (Col A B E) by (forward_using lemma_collinearorder).
assert (Par G K E B) by (conclude lemma_collinearparallel).
assert (Par E B G K) by (conclude lemma_parallelsymmetric).
assert (Par E B K G) by (forward_using lemma_parallelflip).
assert (PG E K G B) by (conclude_def PG ).
close.
Qed.
End Euclid.
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 :
∀ 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 →
PG E K G B.
Proof.
intros.
assert (Par A D B C) by (conclude_def PG ).
assert (Par A B C D) by (conclude_def PG ).
assert (Par E A H K) by (conclude_def PG ).
assert (Par E K A H) by (conclude_def PG ).
assert (Par G K F C) by (conclude_def PG ).
assert (Par F C G K) by (conclude lemma_parallelsymmetric).
assert (Par C F G K) by (forward_using lemma_parallelflip).
assert (Par G C K F) by (conclude_def PG ).
assert (Par B C A D) by (conclude lemma_parallelsymmetric).
assert (Par C D A B) by (conclude lemma_parallelsymmetric).
assert (Par H K E A) by (conclude lemma_parallelsymmetric).
assert (Par A H E K) by (conclude lemma_parallelsymmetric).
assert (Par F C G K) by (conclude lemma_parallelsymmetric).
assert (Par K F G C) by (conclude lemma_parallelsymmetric).
assert (TP A D B C) by (conclude lemma_paralleldef2B).
assert (TP A B C D) by (conclude lemma_paralleldef2B).
assert (TP E A H K) by (conclude lemma_paralleldef2B).
assert (TP E K A H) by (conclude lemma_paralleldef2B).
assert (TP G K F C) by (conclude lemma_paralleldef2B).
assert (TP G C K F) by (conclude lemma_paralleldef2B).
assert (TP B C A D) by (conclude lemma_paralleldef2B).
assert (TP C D A B) by (conclude lemma_paralleldef2B).
assert (TP H K E A) by (conclude lemma_paralleldef2B).
assert (TP A H E K) by (conclude lemma_paralleldef2B).
assert (TP F C G K) by (conclude lemma_paralleldef2B).
assert (TP K F G C) by (conclude lemma_paralleldef2B).
assert (OS A D B C) by (conclude_def TP ).
assert (OS A D C B) by (conclude lemma_samesideflip).
assert (OS D A C B) by (forward_using lemma_samesidesymmetric).
assert (OS A B C D) by (conclude_def TP ).
assert (OS E A H K) by (conclude_def TP ).
assert (OS E K A H) by (conclude_def TP ).
assert (OS G K F C) by (conclude_def TP ).
assert (OS G C K F) by (conclude_def TP ).
assert (OS B C A D) by (conclude_def TP ).
assert (OS C D A B) by (conclude_def TP ).
assert (OS H K E A) by (conclude_def TP ).
assert (OS A H E K) by (conclude_def TP ).
assert (OS F C G K) by (conclude_def TP ).
assert (OS K F G C) by (conclude_def TP ).
assert (neq A E) by (forward_using lemma_betweennotequal).
assert (neq E A) by (conclude lemma_inequalitysymmetric).
assert (neq D F) by (forward_using lemma_betweennotequal).
assert (neq A H) by (forward_using lemma_betweennotequal).
assert (neq B G) by (forward_using lemma_betweennotequal).
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ e, (BetS B A e ∧ Cong A e B A)) by (conclude postulate_extension);destruct Tf as [e];spliter.
assert (BetS e A B) by (conclude axiom_betweennesssymmetry).
assert (OS D C A B) by (forward_using lemma_samesidesymmetric).
assert (RT D A B A B C) by (conclude proposition_29C).
assert (BetS B E A) by (conclude axiom_betweennesssymmetry).
assert (BetS E A e) by (conclude lemma_3_6a).
assert (BetS e A E) by (conclude axiom_betweennesssymmetry).
assert (OS H K A E) by (forward_using lemma_samesidesymmetric).
assert (RT H A E A E K) by (conclude proposition_29C).
assert (Out A E B) by (conclude lemma_ray4).
assert (Out A H D) by (conclude lemma_ray4).
assert (nCol A H E) by (forward_using lemma_parallelNC).
assert (nCol E A H) by (forward_using lemma_NCorder).
assert (CongA E A H E A H) by (conclude lemma_equalanglesreflexive).
assert (CongA E A H B A D) by (conclude lemma_equalangleshelper).
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).
assert (Col D F C) by (conclude_def Col ).
assert (Col D C F) by (forward_using lemma_collinearorder).
assert (OS C D B A) by (conclude lemma_samesideflip).
assert (Col A E B) by (conclude_def Col ).
assert (Col B A E) by (forward_using lemma_collinearorder).
assert (neq E B) by (forward_using lemma_betweennotequal).
assert (neq B E) by (conclude lemma_inequalitysymmetric).
assert (OS C D B E) by (conclude lemma_samesidecollinear).
assert (Out A H D) by (conclude lemma_ray4).
assert (Out A D H) by (conclude lemma_ray5).
assert (OS C H B E) by (conclude lemma_sameside2).
assert (Col E A B) by (forward_using lemma_collinearorder).
assert (OS H K E B) by (conclude lemma_samesidecollinear).
assert (OS H K B E) by (conclude lemma_samesideflip).
assert (OS C K B E) by (conclude lemma_samesidetransitive).
assert (OS K C B E) by (forward_using lemma_samesidesymmetric).
assert (Out B G C) by (conclude lemma_ray4).
assert (Out B C G) by (conclude lemma_ray5).
assert (eq B B) by (conclude cn_equalityreflexive).
assert (Col B B E) by (conclude_def Col ).
assert (OS K G B E) by (conclude lemma_sameside2).
assert (OS K G E B) by (conclude lemma_samesideflip).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Out B E A) by (conclude lemma_ray4).
assert (Out B A E) by (conclude lemma_ray5).
assert (CongA A E K E B G) by (conclude lemma_equalangleshelper).
assert (Par E K B G) by (conclude proposition_28D).
assert (Par E K G B) by (forward_using lemma_parallelflip).
assert (neq B C) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:∃ c, (BetS B C c ∧ Cong C c B C)) by (conclude postulate_extension);destruct Tf as [c];spliter.
assert (BetS c C B) by (conclude axiom_betweennesssymmetry).
assert (Par C D B A) by (forward_using lemma_parallelflip).
assert (RT D C B C B A) by (conclude proposition_29C).
assert (OS K F C G) by (conclude lemma_samesideflip).
assert (OS F K C G) by (forward_using lemma_samesidesymmetric).
assert (BetS C G B) by (conclude axiom_betweennesssymmetry).
assert (BetS c C G) by (conclude axiom_innertransitivity).
assert (RT F C G C G K) by (conclude proposition_29C).
assert (nCol D B C) by (forward_using lemma_parallelNC).
assert (nCol D C B) by (forward_using lemma_NCorder).
assert (CongA D C B D C B) by (conclude lemma_equalanglesreflexive).
assert (BetS C F D) by (conclude axiom_betweennesssymmetry).
assert (neq C F) by (forward_using lemma_betweennotequal).
assert (Out C F D) by (conclude lemma_ray4).
assert (Out C D F) by (conclude lemma_ray5).
assert (BetS C G B) by (conclude axiom_betweennesssymmetry).
assert (neq C G) by (forward_using lemma_betweennotequal).
assert (Out C G B) by (conclude lemma_ray4).
assert (Out C B G) by (conclude lemma_ray5).
assert (CongA D C B F C G) by (conclude lemma_equalangleshelper).
assert (CongA C B A C G K) by (conclude (lemma_supplements2 D C B C G K F C G C B A)).
assert (CongA C G K C B A) by (conclude lemma_equalanglessymmetric).
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Out B A A) by (conclude lemma_ray4).
assert (neq B G) by (forward_using lemma_betweennotequal).
assert (Out B G C) by (conclude lemma_ray4).
assert (Out B C G) by (conclude lemma_ray5).
assert (CongA C G K G B A) by (conclude lemma_equalangleshelper).
assert (Col B G C) by (conclude_def Col ).
assert (Col C B G) by (forward_using lemma_collinearorder).
assert (neq B G) by (forward_using lemma_betweennotequal).
assert (neq G B) by (conclude lemma_inequalitysymmetric).
assert (Par A D C B) by (forward_using lemma_parallelflip).
assert (Par A D G B) by (conclude lemma_collinearparallel).
assert (Par A D B G) by (forward_using lemma_parallelflip).
assert (Par B G A D) by (conclude lemma_parallelsymmetric).
assert (Par G B D A) by (forward_using lemma_parallelflip).
assert (Col A H D) by (conclude_def Col ).
assert (Col D A H) by (forward_using lemma_collinearorder).
assert (neq H A) by (conclude lemma_inequalitysymmetric).
assert (Par G B H A) by (conclude lemma_collinearparallel).
assert (TP G B H A) by (conclude lemma_paralleldef2B).
assert (OS H A G B) by (conclude_def TP ).
assert (BetS C F D) by (conclude axiom_betweennesssymmetry).
assert (neq C F) by (forward_using lemma_betweennotequal).
assert (Out C F D) by (conclude lemma_ray4).
assert (Out C D F) by (conclude lemma_ray5).
assert (eq C C) by (conclude cn_equalityreflexive).
assert (Col B C C) by (conclude_def Col ).
assert (OS A F B C) by (conclude lemma_sameside2).
assert (TP G C K F) by (conclude lemma_paralleldef2B).
assert (OS K F G C) by (conclude_def TP ).
assert (Col B G C) by (conclude_def Col ).
assert (Col C G B) by (forward_using lemma_collinearorder).
assert (neq C B) by (conclude lemma_inequalitysymmetric).
assert (OS K F C G) by (conclude lemma_samesideflip).
assert (OS K F C B) by (conclude lemma_samesidecollinear).
assert (OS K F B C) by (conclude lemma_samesideflip).
assert (OS F K B C) by (forward_using lemma_samesidesymmetric).
assert (OS A K B C) by (conclude lemma_samesidetransitive).
assert (OS K A B C) by (forward_using lemma_samesidesymmetric).
assert (Col B C G) by (forward_using lemma_collinearorder).
assert (OS K A B G) by (conclude lemma_samesidecollinear).
assert (OS K A G B) by (conclude lemma_samesideflip).
assert (Par G K B A) by (conclude proposition_28D).
assert (Par G K A B) by (forward_using lemma_parallelflip).
assert (Col A E B) by (conclude_def Col ).
assert (Col A B E) by (forward_using lemma_collinearorder).
assert (Par G K E B) by (conclude lemma_collinearparallel).
assert (Par E B G K) by (conclude lemma_parallelsymmetric).
assert (Par E B K G) by (forward_using lemma_parallelflip).
assert (PG E K G B) by (conclude_def PG ).
close.
Qed.
End Euclid.