# Library GeoCoq.Elements.OriginalProofs.proposition_45

Require Export GeoCoq.Elements.OriginalProofs.proposition_44.

Require Export GeoCoq.Elements.OriginalProofs.lemma_RTcongruence.

Require Export GeoCoq.Elements.OriginalProofs.lemma_RTsymmetric.

Require Export GeoCoq.Elements.OriginalProofs.proposition_14.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_45 :

∀ A B C D E J K N R S,

nCol J E N → nCol A B D → nCol C B D → TS C B D A → neq R K → nCol K R S →

∃ X Z U, PG X K Z U ∧ CongA X K Z J E N ∧ EF X K Z U A B C D ∧ Out K R Z ∧ OS X S K Z.

Proof.

intros.

assert (Triangle A B D) by (conclude_def Triangle ).

assert (neq B D) by (forward_using lemma_NCdistinct).

let Tf:=fresh in

assert (Tf:∃ m, (BetS B m D ∧ Cong m B m D)) by (conclude proposition_10);destruct Tf as [m];spliter.

assert (Cong B m m D) by (forward_using lemma_congruenceflip).

assert (Midpoint B m D) by (conclude_def Midpoint ).

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

let Tf:=fresh in

assert (Tf:∃ P, (BetS R K P ∧ Cong K P B m)) by (conclude postulate_extension);destruct Tf as [P];spliter.

assert (Triangle A B D) by (conclude_def Triangle ).

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

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

rename_H H;let Tf:=fresh in

assert (Tf:∃ H, (BetS P K H ∧ Cong K H P K)) by (conclude postulate_extension);destruct Tf as [H];spliter.

assert (Cong P K K H) by (conclude lemma_congruencesymmetric).

assert (Midpoint P K H) by (conclude_def Midpoint ).

assert (Cong P K B m) by (forward_using lemma_congruenceflip).

assert (Cong K H B m) by (conclude lemma_congruencetransitive).

assert (Cong B m m D) by (forward_using lemma_congruenceflip).

assert (Cong K H m D) by (conclude lemma_congruencetransitive).

assert (BetS P K R) by (conclude axiom_betweennesssymmetry).

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

assert (Col P K R) by (conclude_def Col ).

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

assert (Col K H R) by (conclude lemma_collinear4).

assert (Col R K H) by (forward_using lemma_collinearorder).

assert (nCol R K S) by (forward_using lemma_NCorder).

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

assert (Col R K K) by (conclude_def Col ).

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

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

assert (nCol H K S) by (conclude lemma_NChelper).

assert (nCol S K H) by (forward_using lemma_NCorder).

let Tf:=fresh in

assert (Tf:∃ F G, (PG F K H G ∧ EF A B m D F K H G ∧ CongA H K F J E N ∧ OS S F K H)) by (conclude proposition_42B);destruct Tf as [F[G]];spliter.

assert (nCol D B C) by (forward_using lemma_NCorder).

assert (Triangle D B C) by (conclude_def Triangle ).

assert (Col R K P) by (conclude_def Col ).

assert (Par F K H G) by (conclude_def PG ).

assert (nCol K H G) by (forward_using lemma_parallelNC).

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

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

let Tf:=fresh in

assert (Tf:∃ M L e, (PG G H M L ∧ CongA G H M J E N ∧ EF D B e C G H M L ∧ Midpoint B e C ∧ TS M G H K)) by (conclude proposition_44);destruct Tf as [M[L[e]]];spliter.

assert (BetS B e C) by (conclude_def Midpoint ).

assert (CongA J E N G H M) by (conclude lemma_equalanglessymmetric).

assert (CongA H K F G H M) by (conclude lemma_equalanglestransitive).

assert (Par F K H G) by (conclude_def PG ).

assert (Par K F H G) by (forward_using lemma_parallelflip).

assert (neq H K) by (forward_using lemma_NCdistinct).

let Tf:=fresh in

assert (Tf:∃ s, (BetS H K s ∧ Cong K s H K)) by (conclude postulate_extension);destruct Tf as [s];spliter.

assert (Par F G K H) by (conclude_def PG ).

assert (Par K H F G) by (conclude lemma_parallelsymmetric).

assert (TP K H F G) by (conclude lemma_paralleldef2B).

assert (OS F G K H) by (conclude_def TP ).

assert (RT F K H K H G) by (conclude proposition_29C).

assert (CongA G H M H K F) by (conclude lemma_equalanglessymmetric).

assert (nCol H K F) by (conclude lemma_equalanglesNC).

assert (nCol F K H) by (forward_using lemma_NCorder).

assert (CongA F K H H K F) by (conclude lemma_ABCequalsCBA).

assert (CongA F K H G H M) by (conclude lemma_equalanglestransitive).

assert (RT G H M K H G) by (conclude lemma_RTcongruence).

assert (RT K H G G H M) by (conclude lemma_RTsymmetric).

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

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

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

assert (BetS K H M) by (conclude proposition_14).

assert (neq F K) by (forward_using lemma_NCdistinct).

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

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

assert (Par G H M L) by (conclude_def PG ).

assert (nCol H M L) by (forward_using lemma_parallelNC).

assert (neq L M) by (forward_using lemma_NCdistinct).

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

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

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

assert (Col F K K) by (conclude_def Col ).

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

assert (Col L M M) by (conclude_def Col ).

assert (Par F K G H) by (forward_using lemma_parallelflip).

assert (Par M L G H) by (conclude lemma_parallelsymmetric).

assert (Par L M G H) by (forward_using lemma_parallelflip).

assert (Par F K L M) by (conclude proposition_30).

assert (Par F K M L) by (forward_using lemma_parallelflip).

assert (Par F G K H) by (conclude_def PG ).

assert (Par G L H M) by (conclude_def PG ).

assert (Par F G H K) by (forward_using lemma_parallelflip).

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

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

assert (neq K M) by (forward_using lemma_betweennotequal).

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

assert (Par F G M K) by (conclude lemma_collinearparallel).

assert (Par F G K M) by (forward_using lemma_parallelflip).

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

assert (Par G L K M) by (conclude lemma_collinearparallel).

assert (Par G L M K) by (forward_using lemma_parallelflip).

assert (Par M K G L) by (conclude lemma_parallelsymmetric).

assert (Par M K F G) by (conclude lemma_parallelsymmetric).

assert (Par M K G F) by (forward_using lemma_parallelflip).

assert (Col G L F) by (conclude lemma_Playfair).

assert (Col G F L) by (forward_using lemma_collinearorder).

assert (nCol F L M) by (forward_using lemma_parallelNC).

assert (neq L F) by (forward_using lemma_NCdistinct).

assert (Par M K L F) by (conclude lemma_collinearparallel).

assert (Par L F M K) by (conclude lemma_parallelsymmetric).

assert (Par F L K M) by (forward_using lemma_parallelflip).

assert (PG F K M L) by (conclude_def PG ).

assert (nCol F K H) by (forward_using lemma_parallelNC).

assert (CongA F K H H K F) by (conclude lemma_ABCequalsCBA).

assert (CongA F K H J E N) by (conclude lemma_equalanglestransitive).

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

assert (Out K H M) by (conclude lemma_ray4).

assert (Out K M H) by (conclude lemma_ray5).

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

assert (neq K F) by (forward_using lemma_NCdistinct).

assert (Out K F F) by (conclude lemma_ray4).

assert (nCol F K M) by (forward_using lemma_parallelNC).

assert (CongA F K M F K M) by (conclude lemma_equalanglesreflexive).

assert (CongA F K M F K H) by (conclude lemma_equalangleshelper).

assert (CongA F K M J E N) by (conclude lemma_equalanglestransitive).

assert (TS A B D C) by (conclude lemma_oppositesidesymmetric).

assert (Par G H L M) by (forward_using lemma_parallelflip).

assert (TP G H L M) by (conclude lemma_paralleldef2B).

assert (OS L M G H) by (conclude_def TP ).

assert (Par F K G H) by (forward_using lemma_parallelflip).

assert (Par G H F K) by (conclude lemma_parallelsymmetric).

assert (TP G H F K) by (conclude lemma_paralleldef2B).

assert (OS F K G H) by (conclude_def TP ).

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

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

assert (nCol K G H) by (forward_using lemma_parallelNC).

assert (TS K G H M) by (conclude_def TS ).

assert (TS F G H M) by (conclude lemma_planeseparation).

assert (TS M G H F) by (conclude lemma_oppositesidesymmetric).

assert (TS L G H F) by (conclude lemma_planeseparation).

let Tf:=fresh in

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

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

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

assert (Col F L G) by (forward_using lemma_collinearorder).

assert (Col L t F) by (conclude_def Col ).

assert (Col F L t) by (forward_using lemma_collinearorder).

assert (neq F L) by (forward_using lemma_NCdistinct).

assert (Col L G t) by (conclude lemma_collinear4).

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

assert (Col t G L) by (forward_using lemma_collinearorder).

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

assert (¬ neq t G).

{

intro.

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

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

contradict.

}

assert (BetS L G F) by (conclude cn_equalitysub).

assert (BetS F G L) by (conclude axiom_betweennesssymmetry).

assert (EF A B C D F K M L) by (conclude axiom_paste4).

assert (EF F K M L A B C D) by (conclude axiom_EFsymmetric).

assert (BetS H K P) by (conclude axiom_betweennesssymmetry).

assert (neq K R) by (conclude lemma_inequalitysymmetric).

assert (BetS P K M) by (conclude lemma_3_7b).

assert (Out K R M) by (conclude_def Out ).

assert (OS F S K H) by (forward_using lemma_samesidesymmetric).

assert (OS F S H K) by (conclude lemma_samesideflip).

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

assert (Col P K R) by (conclude_def Col ).

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

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

assert (OS F S K M) by (conclude lemma_samesidecollinear).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_RTcongruence.

Require Export GeoCoq.Elements.OriginalProofs.lemma_RTsymmetric.

Require Export GeoCoq.Elements.OriginalProofs.proposition_14.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_45 :

∀ A B C D E J K N R S,

nCol J E N → nCol A B D → nCol C B D → TS C B D A → neq R K → nCol K R S →

∃ X Z U, PG X K Z U ∧ CongA X K Z J E N ∧ EF X K Z U A B C D ∧ Out K R Z ∧ OS X S K Z.

Proof.

intros.

assert (Triangle A B D) by (conclude_def Triangle ).

assert (neq B D) by (forward_using lemma_NCdistinct).

let Tf:=fresh in

assert (Tf:∃ m, (BetS B m D ∧ Cong m B m D)) by (conclude proposition_10);destruct Tf as [m];spliter.

assert (Cong B m m D) by (forward_using lemma_congruenceflip).

assert (Midpoint B m D) by (conclude_def Midpoint ).

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

let Tf:=fresh in

assert (Tf:∃ P, (BetS R K P ∧ Cong K P B m)) by (conclude postulate_extension);destruct Tf as [P];spliter.

assert (Triangle A B D) by (conclude_def Triangle ).

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

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

rename_H H;let Tf:=fresh in

assert (Tf:∃ H, (BetS P K H ∧ Cong K H P K)) by (conclude postulate_extension);destruct Tf as [H];spliter.

assert (Cong P K K H) by (conclude lemma_congruencesymmetric).

assert (Midpoint P K H) by (conclude_def Midpoint ).

assert (Cong P K B m) by (forward_using lemma_congruenceflip).

assert (Cong K H B m) by (conclude lemma_congruencetransitive).

assert (Cong B m m D) by (forward_using lemma_congruenceflip).

assert (Cong K H m D) by (conclude lemma_congruencetransitive).

assert (BetS P K R) by (conclude axiom_betweennesssymmetry).

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

assert (Col P K R) by (conclude_def Col ).

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

assert (Col K H R) by (conclude lemma_collinear4).

assert (Col R K H) by (forward_using lemma_collinearorder).

assert (nCol R K S) by (forward_using lemma_NCorder).

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

assert (Col R K K) by (conclude_def Col ).

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

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

assert (nCol H K S) by (conclude lemma_NChelper).

assert (nCol S K H) by (forward_using lemma_NCorder).

let Tf:=fresh in

assert (Tf:∃ F G, (PG F K H G ∧ EF A B m D F K H G ∧ CongA H K F J E N ∧ OS S F K H)) by (conclude proposition_42B);destruct Tf as [F[G]];spliter.

assert (nCol D B C) by (forward_using lemma_NCorder).

assert (Triangle D B C) by (conclude_def Triangle ).

assert (Col R K P) by (conclude_def Col ).

assert (Par F K H G) by (conclude_def PG ).

assert (nCol K H G) by (forward_using lemma_parallelNC).

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

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

let Tf:=fresh in

assert (Tf:∃ M L e, (PG G H M L ∧ CongA G H M J E N ∧ EF D B e C G H M L ∧ Midpoint B e C ∧ TS M G H K)) by (conclude proposition_44);destruct Tf as [M[L[e]]];spliter.

assert (BetS B e C) by (conclude_def Midpoint ).

assert (CongA J E N G H M) by (conclude lemma_equalanglessymmetric).

assert (CongA H K F G H M) by (conclude lemma_equalanglestransitive).

assert (Par F K H G) by (conclude_def PG ).

assert (Par K F H G) by (forward_using lemma_parallelflip).

assert (neq H K) by (forward_using lemma_NCdistinct).

let Tf:=fresh in

assert (Tf:∃ s, (BetS H K s ∧ Cong K s H K)) by (conclude postulate_extension);destruct Tf as [s];spliter.

assert (Par F G K H) by (conclude_def PG ).

assert (Par K H F G) by (conclude lemma_parallelsymmetric).

assert (TP K H F G) by (conclude lemma_paralleldef2B).

assert (OS F G K H) by (conclude_def TP ).

assert (RT F K H K H G) by (conclude proposition_29C).

assert (CongA G H M H K F) by (conclude lemma_equalanglessymmetric).

assert (nCol H K F) by (conclude lemma_equalanglesNC).

assert (nCol F K H) by (forward_using lemma_NCorder).

assert (CongA F K H H K F) by (conclude lemma_ABCequalsCBA).

assert (CongA F K H G H M) by (conclude lemma_equalanglestransitive).

assert (RT G H M K H G) by (conclude lemma_RTcongruence).

assert (RT K H G G H M) by (conclude lemma_RTsymmetric).

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

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

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

assert (BetS K H M) by (conclude proposition_14).

assert (neq F K) by (forward_using lemma_NCdistinct).

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

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

assert (Par G H M L) by (conclude_def PG ).

assert (nCol H M L) by (forward_using lemma_parallelNC).

assert (neq L M) by (forward_using lemma_NCdistinct).

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

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

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

assert (Col F K K) by (conclude_def Col ).

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

assert (Col L M M) by (conclude_def Col ).

assert (Par F K G H) by (forward_using lemma_parallelflip).

assert (Par M L G H) by (conclude lemma_parallelsymmetric).

assert (Par L M G H) by (forward_using lemma_parallelflip).

assert (Par F K L M) by (conclude proposition_30).

assert (Par F K M L) by (forward_using lemma_parallelflip).

assert (Par F G K H) by (conclude_def PG ).

assert (Par G L H M) by (conclude_def PG ).

assert (Par F G H K) by (forward_using lemma_parallelflip).

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

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

assert (neq K M) by (forward_using lemma_betweennotequal).

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

assert (Par F G M K) by (conclude lemma_collinearparallel).

assert (Par F G K M) by (forward_using lemma_parallelflip).

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

assert (Par G L K M) by (conclude lemma_collinearparallel).

assert (Par G L M K) by (forward_using lemma_parallelflip).

assert (Par M K G L) by (conclude lemma_parallelsymmetric).

assert (Par M K F G) by (conclude lemma_parallelsymmetric).

assert (Par M K G F) by (forward_using lemma_parallelflip).

assert (Col G L F) by (conclude lemma_Playfair).

assert (Col G F L) by (forward_using lemma_collinearorder).

assert (nCol F L M) by (forward_using lemma_parallelNC).

assert (neq L F) by (forward_using lemma_NCdistinct).

assert (Par M K L F) by (conclude lemma_collinearparallel).

assert (Par L F M K) by (conclude lemma_parallelsymmetric).

assert (Par F L K M) by (forward_using lemma_parallelflip).

assert (PG F K M L) by (conclude_def PG ).

assert (nCol F K H) by (forward_using lemma_parallelNC).

assert (CongA F K H H K F) by (conclude lemma_ABCequalsCBA).

assert (CongA F K H J E N) by (conclude lemma_equalanglestransitive).

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

assert (Out K H M) by (conclude lemma_ray4).

assert (Out K M H) by (conclude lemma_ray5).

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

assert (neq K F) by (forward_using lemma_NCdistinct).

assert (Out K F F) by (conclude lemma_ray4).

assert (nCol F K M) by (forward_using lemma_parallelNC).

assert (CongA F K M F K M) by (conclude lemma_equalanglesreflexive).

assert (CongA F K M F K H) by (conclude lemma_equalangleshelper).

assert (CongA F K M J E N) by (conclude lemma_equalanglestransitive).

assert (TS A B D C) by (conclude lemma_oppositesidesymmetric).

assert (Par G H L M) by (forward_using lemma_parallelflip).

assert (TP G H L M) by (conclude lemma_paralleldef2B).

assert (OS L M G H) by (conclude_def TP ).

assert (Par F K G H) by (forward_using lemma_parallelflip).

assert (Par G H F K) by (conclude lemma_parallelsymmetric).

assert (TP G H F K) by (conclude lemma_paralleldef2B).

assert (OS F K G H) by (conclude_def TP ).

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

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

assert (nCol K G H) by (forward_using lemma_parallelNC).

assert (TS K G H M) by (conclude_def TS ).

assert (TS F G H M) by (conclude lemma_planeseparation).

assert (TS M G H F) by (conclude lemma_oppositesidesymmetric).

assert (TS L G H F) by (conclude lemma_planeseparation).

let Tf:=fresh in

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

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

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

assert (Col F L G) by (forward_using lemma_collinearorder).

assert (Col L t F) by (conclude_def Col ).

assert (Col F L t) by (forward_using lemma_collinearorder).

assert (neq F L) by (forward_using lemma_NCdistinct).

assert (Col L G t) by (conclude lemma_collinear4).

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

assert (Col t G L) by (forward_using lemma_collinearorder).

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

assert (¬ neq t G).

{

intro.

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

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

contradict.

}

assert (BetS L G F) by (conclude cn_equalitysub).

assert (BetS F G L) by (conclude axiom_betweennesssymmetry).

assert (EF A B C D F K M L) by (conclude axiom_paste4).

assert (EF F K M L A B C D) by (conclude axiom_EFsymmetric).

assert (BetS H K P) by (conclude axiom_betweennesssymmetry).

assert (neq K R) by (conclude lemma_inequalitysymmetric).

assert (BetS P K M) by (conclude lemma_3_7b).

assert (Out K R M) by (conclude_def Out ).

assert (OS F S K H) by (forward_using lemma_samesidesymmetric).

assert (OS F S H K) by (conclude lemma_samesideflip).

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

assert (Col P K R) by (conclude_def Col ).

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

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

assert (OS F S K M) by (conclude lemma_samesidecollinear).

close.

Qed.

End Euclid.