# Library GeoCoq.Elements.OriginalProofs.proposition_42

Require Export GeoCoq.Elements.OriginalProofs.lemma_samesidecollinear.

Require Export GeoCoq.Elements.OriginalProofs.lemma_PGflip.

Require Export GeoCoq.Elements.OriginalProofs.proposition_41.

Require Export GeoCoq.Elements.OriginalProofs.proposition_38.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_42 :

∀ A B C D E J K,

Triangle A B C → nCol J D K → Midpoint B E C →

∃ X Z, PG X E C Z ∧ EF A B E C X E C Z ∧ CongA C E X J D K ∧ Col X Z A.

Proof.

intros.

assert ((BetS B E C ∧ Cong B E E C)) by (conclude_def Midpoint ).

assert (Cong E B E C) by (forward_using lemma_congruenceflip).

assert (nCol A B C) by (conclude_def Triangle ).

assert (Col B E C) by (conclude_def Col ).

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

assert (Col B C E) by (forward_using lemma_collinearorder).

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

assert (Col B C C) by (conclude_def Col ).

assert (neq E C) by (forward_using lemma_betweennotequal).

assert (nCol E C A) by (conclude lemma_NChelper).

let Tf:=fresh in

assert (Tf:∃ f c, (Out E C c ∧ CongA f E c J D K ∧ OS f A E C)) by (conclude proposition_23C);destruct Tf as [f[c]];spliter.

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

let Tf:=fresh in

assert (Tf:∃ P Q M, (BetS P A Q ∧ CongA Q A E A E B ∧ CongA Q A E B E A ∧ CongA E A Q B E A ∧ CongA P A E A E C ∧ CongA P A E C E A ∧ CongA E A P C E A ∧ Par P Q B C ∧ Cong P A E C ∧ Cong A Q B E ∧ Cong A M M E ∧ Cong P M M C ∧ Cong B M M Q ∧ BetS P M C ∧ BetS B M Q ∧ BetS A M E)) by (conclude proposition_31);destruct Tf as [P[Q[M]]];spliter.

assert (CongA A E C P A E) by (conclude lemma_equalanglessymmetric).

assert (nCol P A E) by (conclude lemma_equalanglesNC).

assert (nCol E A P) by (forward_using lemma_NCorder).

assert (OS A f E C) by (forward_using lemma_samesidesymmetric).

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

assert (Col B C E) by (forward_using lemma_collinearorder).

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

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

assert (Col B C B) by (conclude_def Col ).

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

assert (nCol B E A) by (conclude lemma_NChelper).

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

assert (Col B C C) by (conclude_def Col ).

assert (neq E C) by (forward_using lemma_betweennotequal).

assert (neq C E) by (conclude lemma_inequalitysymmetric).

assert (nCol C E A) by (conclude lemma_NChelper).

assert (neq E A) by (forward_using lemma_NCdistinct).

assert (¬ ¬ Meet E f P Q).

{

intro.

assert (¬ LtA C E f C E A).

{

intro.

assert (Out E C C) by (conclude lemma_ray4).

assert (Out E A A) by (conclude lemma_ray4).

let Tf:=fresh in

assert (Tf:∃ m, (BetS A m C ∧ Out E f m)) by (conclude lemma_crossbar2);destruct Tf as [m];spliter.

assert (BetS C m A) by (conclude axiom_betweennesssymmetry).

assert (BetS C M P) by (conclude axiom_betweennesssymmetry).

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

assert (Cong M E A M) by (conclude lemma_congruencesymmetric).

assert (Cong E M A M) by (forward_using lemma_congruenceflip).

assert (Cong M C P M) by (conclude lemma_congruencesymmetric).

assert (Cong M C M P) by (forward_using lemma_congruenceflip).

let Tf:=fresh in

assert (Tf:∃ F, (BetS E m F ∧ BetS P A F)) by (conclude postulate_Euclid5);destruct Tf as [F];spliter.

assert (Col E m F) by (conclude_def Col ).

assert (Col m E F) by (forward_using lemma_collinearorder).

assert (Col E f m) by (conclude lemma_rayimpliescollinear).

assert (Col m E f) by (forward_using lemma_collinearorder).

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

assert (neq m E) by (conclude lemma_inequalitysymmetric).

assert (Col E f F) by (conclude lemma_collinear4).

assert (Col P A F) by (conclude_def Col ).

assert (Col P A Q) by (conclude_def Col ).

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

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

assert (Col A P F) by (forward_using lemma_collinearorder).

assert (Col A P Q) by (forward_using lemma_collinearorder).

assert (Col P F Q) by (conclude lemma_collinear4).

assert (Col P Q F) by (forward_using lemma_collinearorder).

assert (neq E f) by (conclude lemma_ray2).

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

assert (Meet E f P Q) by (conclude_def Meet ).

contradict.

}

assert (Col E C B) by (forward_using lemma_collinearorder).

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

assert (neq E B) by (conclude lemma_inequalitysymmetric).

assert (OS A f E B) by (conclude lemma_samesidecollinear).

assert (OS f A E B) by (forward_using lemma_samesidesymmetric).

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

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

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

assert (nCol E B f) by (conclude_def OS ).

assert (neq E f) by (forward_using lemma_NCdistinct).

assert (Col B E C) by (conclude_def Col ).

assert (Col E B C) by (forward_using lemma_collinearorder).

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

assert (Col E B E) by (conclude_def Col ).

assert (nCol E C f) by (conclude lemma_NChelper).

assert (nCol C E f) by (forward_using lemma_NCorder).

assert (¬ LtA C E A C E f).

{

intro.

assert (Out E A A) by (conclude lemma_ray4).

assert (Out E f f) by (conclude lemma_ray4).

assert (Supp C E A A B) by (conclude_def Supp ).

assert (Supp C E f f B) by (conclude_def Supp ).

assert (LtA f E B A E B) by (conclude lemma_supplementinequality).

assert (nCol B E f) by (forward_using lemma_NCorder).

assert (CongA B E f f E B) by (conclude lemma_ABCequalsCBA).

assert (LtA B E f A E B) by (conclude lemma_angleorderrespectscongruence2).

assert (CongA B E A A E B) by (conclude lemma_ABCequalsCBA).

assert (LtA B E f B E A) by (conclude lemma_angleorderrespectscongruence).

assert (Out E B B) by (conclude lemma_ray4).

assert (Out E A A) by (conclude lemma_ray4).

let Tf:=fresh in

assert (Tf:∃ m, (BetS A m B ∧ Out E f m)) by (conclude lemma_crossbar2);destruct Tf as [m];spliter.

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

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

assert (Cong M E A M) by (conclude lemma_congruencesymmetric).

assert (Cong E M A M) by (forward_using lemma_congruenceflip).

assert (Cong M B M Q) by (forward_using lemma_congruenceflip).

assert (nCol P A E) by (forward_using lemma_NCorder).

assert (Col P A Q) by (conclude_def Col ).

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

assert (Col P A A) by (conclude_def Col ).

assert (neq A Q) by (forward_using lemma_betweennotequal).

assert (neq Q A) by (conclude lemma_inequalitysymmetric).

assert (nCol Q A E) by (conclude lemma_NChelper).

assert (nCol E A Q) by (forward_using lemma_NCorder).

let Tf:=fresh in

assert (Tf:∃ F, (BetS E m F ∧ BetS Q A F)) by (conclude postulate_Euclid5);destruct Tf as [F];spliter.

assert (Col E m F) by (conclude_def Col ).

assert (Col m E F) by (forward_using lemma_collinearorder).

assert (Col E f m) by (conclude lemma_rayimpliescollinear).

assert (Col m E f) by (forward_using lemma_collinearorder).

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

assert (neq m E) by (conclude lemma_inequalitysymmetric).

assert (Col E f F) by (conclude lemma_collinear4).

assert (Col Q A F) by (conclude_def Col ).

assert (BetS Q A P) by (conclude axiom_betweennesssymmetry).

assert (Col Q A P) by (conclude_def Col ).

assert (neq Q A) by (forward_using lemma_betweennotequal).

assert (neq A Q) by (conclude lemma_inequalitysymmetric).

assert (Col A Q F) by (forward_using lemma_collinearorder).

assert (Col A Q P) by (forward_using lemma_collinearorder).

assert (Col Q F P) by (conclude lemma_collinear4).

assert (Col P Q F) by (forward_using lemma_collinearorder).

assert (neq E f) by (conclude lemma_ray2).

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

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

assert (Meet E f P Q) by (conclude_def Meet ).

contradict.

}

assert (¬ ¬ CongA C E A C E f).

{

intro.

assert (LtA C E A C E f) by (conclude lemma_angletrichotomy2).

contradict.

}

let Tf:=fresh in

assert (Tf:∃ a d p q, (Out E C d ∧ Out E A a ∧ Out E C p ∧ Out E f q ∧ Cong E d E p ∧ Cong E a E q ∧ Cong d a p q ∧ nCol C E A)) by (conclude_def CongA );destruct Tf as [a[d[p[q]]]];spliter.

assert (Col P Q A) by (conclude_def Col ).

assert (eq d p) by (conclude lemma_layoffunique).

assert (Cong d a d q) by (conclude cn_equalitysub).

assert (Cong a d q d) by (forward_using lemma_congruenceflip).

assert (Cong a E q E) by (forward_using lemma_congruenceflip).

assert (neq E d) by (conclude lemma_raystrict).

assert (Col E C d) by (conclude lemma_rayimpliescollinear).

assert (OS A f E d) by (conclude lemma_samesidecollinear).

assert (Col E d E) by (conclude_def Col ).

assert (Col E E d) by (forward_using lemma_collinearorder).

assert (OS A q E d) by (conclude lemma_sameside2).

assert (OS q A E d) by (forward_using lemma_samesidesymmetric).

assert (OS q a E d) by (conclude lemma_sameside2).

assert (OS a q E d) by (forward_using lemma_samesidesymmetric).

assert (eq a q) by (conclude proposition_07).

assert (Col E A a) by (conclude lemma_rayimpliescollinear).

assert (Col E f q) by (conclude lemma_rayimpliescollinear).

assert (Col E A q) by (conclude cn_equalitysub).

assert (Col q E A) by (forward_using lemma_collinearorder).

assert (Col q E f) by (forward_using lemma_collinearorder).

assert (neq E q) by (conclude lemma_raystrict).

assert (neq q E) by (conclude lemma_inequalitysymmetric).

assert (Col E A f) by (conclude lemma_collinear4).

assert (Col E f A) by (forward_using lemma_collinearorder).

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

assert (Meet E f P Q) by (conclude_def Meet ).

contradict.

}

let Tf:=fresh in

assert (Tf:∃ F, (neq E f ∧ neq P Q ∧ Col E f F ∧ Col P Q F)) by (conclude_def Meet );destruct Tf as [F];spliter.

assert (neq C E) by (conclude lemma_inequalitysymmetric).

assert (Par P Q E C) by (conclude lemma_collinearparallel).

assert (Par E C P Q) by (conclude lemma_parallelsymmetric).

let Tf:=fresh in

assert (Tf:∃ G, (PG F G C E ∧ Col P Q G)) by (conclude lemma_triangletoparallelogram);destruct Tf as [G];spliter.

assert (PG G F E C) by (conclude lemma_PGflip).

assert (PG F E C G) by (conclude lemma_PGrotate).

assert (Col P A Q) by (conclude_def Col ).

assert (Col P Q A) by (forward_using lemma_collinearorder).

assert (Par F E C G) by (conclude_def PG ).

assert (nCol F E G) by (forward_using lemma_parallelNC).

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

assert (Col F G A) by (conclude lemma_collinear5).

assert (ET F E C A E C) by (conclude proposition_41).

assert (Par P Q C B) by (forward_using lemma_parallelflip).

assert (Col C B E) by (forward_using lemma_collinearorder).

assert (neq E B) by (conclude lemma_inequalitysymmetric).

assert (Par P Q E B) by (conclude lemma_collinearparallel).

assert (Par P Q B E) by (forward_using lemma_parallelflip).

assert (Cong B E E C) by (forward_using lemma_congruenceflip).

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

assert (Col B E E) by (conclude_def Col ).

assert (ET A B E A E C) by (conclude proposition_38).

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

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

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

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

assert (Col A E E) by (conclude_def Col ).

assert (nCol A E B) by (forward_using lemma_NCorder).

assert (TS B A E C) by (conclude_def TS ).

assert (PG E F G C) by (conclude lemma_PGflip).

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

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

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

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

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

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

let Tf:=fresh in

assert (Tf:∃ m, (BetS E m G ∧ BetS F m C)) by (conclude lemma_diagonalsmeet);destruct Tf as [m];spliter.

assert (Col F m C) by (conclude_def Col ).

assert (Col F C m) by (forward_using lemma_collinearorder).

assert (Par F E C G) by (conclude_def PG ).

assert (nCol F E C) by (forward_using lemma_parallelNC).

assert (nCol F C E) by (forward_using lemma_NCorder).

assert (TS E F C G) by (conclude_def TS ).

assert (ET A E C F E C) by (conclude axiom_ETsymmetric).

assert (ET A E B F E C) by (conclude axiom_ETtransitive).

assert (ET A E B F C E) by (forward_using axiom_ETpermutation).

assert (ET A E C F E C) by (conclude axiom_ETsymmetric).

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

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

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

assert (ET A E C F C G) by (conclude axiom_ETtransitive).

assert (EF A B E C F E C G) by (conclude axiom_paste3).

assert (nCol F E C) by (forward_using lemma_parallelNC).

assert (nCol C E F) by (forward_using lemma_NCorder).

assert (CongA C E F C E F) by (conclude lemma_equalanglesreflexive).

assert ((eq E f ∨ eq E F ∨ eq f F ∨ BetS f E F ∨ BetS E f F ∨ BetS E F f)) by (conclude_def Col ).

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

assert (neq E F) by (conclude lemma_inequalitysymmetric).

assert (Out E F f).

by cases on (eq E f ∨ eq E F ∨ eq f F ∨ BetS f E F ∨ BetS E f F ∨ BetS E F f).

{

assert (¬ ¬ Out E F f).

{

intro.

contradict.

}

close.

}

{

assert (¬ ¬ Out E F f).

{

intro.

contradict.

}

close.

}

{

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

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

assert (Out E F f) by (conclude cn_equalitysub).

close.

}

{

assert (¬ ¬ Out E F f).

{

intro.

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

assert (Col E C E) by (conclude_def Col ).

assert (BetS F E f) by (conclude axiom_betweennesssymmetry).

assert (nCol E C F) by (forward_using lemma_NCorder).

assert (TS F E C f) by (conclude_def TS ).

assert (TS f E C F) by (conclude lemma_oppositesidesymmetric).

assert (OS A f E C) by (forward_using lemma_samesidesymmetric).

assert (TS A E C F) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ j, (BetS A j F ∧ Col E C j ∧ nCol E C A)) by (conclude_def TS );destruct Tf as [j];spliter.

assert (Col A j F) by (conclude_def Col ).

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

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

assert (Col Q A F) by (conclude lemma_collinear4).

assert (Col A F Q) by (forward_using lemma_collinearorder).

assert (Col Q P A) by (forward_using lemma_collinearorder).

assert (Col Q P F) by (forward_using lemma_collinearorder).

assert (Col P A F) by (conclude lemma_collinear4).

assert (Col A F P) by (forward_using lemma_collinearorder).

assert (Col A F j) by (forward_using lemma_collinearorder).

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

assert (neq A F) by (forward_using lemma_betweennotequal).

assert (Col P Q j) by (conclude lemma_collinear5).

assert (Meet P Q E C) by (conclude_def Meet ).

assert (¬ Meet P Q E C) by (conclude_def Par ).

contradict.

}

close.

}

{

assert (Out E F f) by (conclude lemma_ray4).

close.

}

{

assert (Out E F f) by (conclude lemma_ray4).

close.

}

assert (CongA C E F c E f) by (conclude lemma_equalangleshelper).

assert (CongA F E C f E c) by (conclude lemma_equalanglesflip).

assert (CongA F E C J D K) by (conclude lemma_equalanglestransitive).

assert (CongA C E F F E C) by (conclude lemma_ABCequalsCBA).

assert (CongA C E F J D K) by (conclude lemma_equalanglestransitive).

close.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.lemma_PGflip.

Require Export GeoCoq.Elements.OriginalProofs.proposition_41.

Require Export GeoCoq.Elements.OriginalProofs.proposition_38.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_42 :

∀ A B C D E J K,

Triangle A B C → nCol J D K → Midpoint B E C →

∃ X Z, PG X E C Z ∧ EF A B E C X E C Z ∧ CongA C E X J D K ∧ Col X Z A.

Proof.

intros.

assert ((BetS B E C ∧ Cong B E E C)) by (conclude_def Midpoint ).

assert (Cong E B E C) by (forward_using lemma_congruenceflip).

assert (nCol A B C) by (conclude_def Triangle ).

assert (Col B E C) by (conclude_def Col ).

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

assert (Col B C E) by (forward_using lemma_collinearorder).

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

assert (Col B C C) by (conclude_def Col ).

assert (neq E C) by (forward_using lemma_betweennotequal).

assert (nCol E C A) by (conclude lemma_NChelper).

let Tf:=fresh in

assert (Tf:∃ f c, (Out E C c ∧ CongA f E c J D K ∧ OS f A E C)) by (conclude proposition_23C);destruct Tf as [f[c]];spliter.

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

let Tf:=fresh in

assert (Tf:∃ P Q M, (BetS P A Q ∧ CongA Q A E A E B ∧ CongA Q A E B E A ∧ CongA E A Q B E A ∧ CongA P A E A E C ∧ CongA P A E C E A ∧ CongA E A P C E A ∧ Par P Q B C ∧ Cong P A E C ∧ Cong A Q B E ∧ Cong A M M E ∧ Cong P M M C ∧ Cong B M M Q ∧ BetS P M C ∧ BetS B M Q ∧ BetS A M E)) by (conclude proposition_31);destruct Tf as [P[Q[M]]];spliter.

assert (CongA A E C P A E) by (conclude lemma_equalanglessymmetric).

assert (nCol P A E) by (conclude lemma_equalanglesNC).

assert (nCol E A P) by (forward_using lemma_NCorder).

assert (OS A f E C) by (forward_using lemma_samesidesymmetric).

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

assert (Col B C E) by (forward_using lemma_collinearorder).

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

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

assert (Col B C B) by (conclude_def Col ).

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

assert (nCol B E A) by (conclude lemma_NChelper).

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

assert (Col B C C) by (conclude_def Col ).

assert (neq E C) by (forward_using lemma_betweennotequal).

assert (neq C E) by (conclude lemma_inequalitysymmetric).

assert (nCol C E A) by (conclude lemma_NChelper).

assert (neq E A) by (forward_using lemma_NCdistinct).

assert (¬ ¬ Meet E f P Q).

{

intro.

assert (¬ LtA C E f C E A).

{

intro.

assert (Out E C C) by (conclude lemma_ray4).

assert (Out E A A) by (conclude lemma_ray4).

let Tf:=fresh in

assert (Tf:∃ m, (BetS A m C ∧ Out E f m)) by (conclude lemma_crossbar2);destruct Tf as [m];spliter.

assert (BetS C m A) by (conclude axiom_betweennesssymmetry).

assert (BetS C M P) by (conclude axiom_betweennesssymmetry).

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

assert (Cong M E A M) by (conclude lemma_congruencesymmetric).

assert (Cong E M A M) by (forward_using lemma_congruenceflip).

assert (Cong M C P M) by (conclude lemma_congruencesymmetric).

assert (Cong M C M P) by (forward_using lemma_congruenceflip).

let Tf:=fresh in

assert (Tf:∃ F, (BetS E m F ∧ BetS P A F)) by (conclude postulate_Euclid5);destruct Tf as [F];spliter.

assert (Col E m F) by (conclude_def Col ).

assert (Col m E F) by (forward_using lemma_collinearorder).

assert (Col E f m) by (conclude lemma_rayimpliescollinear).

assert (Col m E f) by (forward_using lemma_collinearorder).

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

assert (neq m E) by (conclude lemma_inequalitysymmetric).

assert (Col E f F) by (conclude lemma_collinear4).

assert (Col P A F) by (conclude_def Col ).

assert (Col P A Q) by (conclude_def Col ).

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

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

assert (Col A P F) by (forward_using lemma_collinearorder).

assert (Col A P Q) by (forward_using lemma_collinearorder).

assert (Col P F Q) by (conclude lemma_collinear4).

assert (Col P Q F) by (forward_using lemma_collinearorder).

assert (neq E f) by (conclude lemma_ray2).

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

assert (Meet E f P Q) by (conclude_def Meet ).

contradict.

}

assert (Col E C B) by (forward_using lemma_collinearorder).

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

assert (neq E B) by (conclude lemma_inequalitysymmetric).

assert (OS A f E B) by (conclude lemma_samesidecollinear).

assert (OS f A E B) by (forward_using lemma_samesidesymmetric).

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

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

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

assert (nCol E B f) by (conclude_def OS ).

assert (neq E f) by (forward_using lemma_NCdistinct).

assert (Col B E C) by (conclude_def Col ).

assert (Col E B C) by (forward_using lemma_collinearorder).

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

assert (Col E B E) by (conclude_def Col ).

assert (nCol E C f) by (conclude lemma_NChelper).

assert (nCol C E f) by (forward_using lemma_NCorder).

assert (¬ LtA C E A C E f).

{

intro.

assert (Out E A A) by (conclude lemma_ray4).

assert (Out E f f) by (conclude lemma_ray4).

assert (Supp C E A A B) by (conclude_def Supp ).

assert (Supp C E f f B) by (conclude_def Supp ).

assert (LtA f E B A E B) by (conclude lemma_supplementinequality).

assert (nCol B E f) by (forward_using lemma_NCorder).

assert (CongA B E f f E B) by (conclude lemma_ABCequalsCBA).

assert (LtA B E f A E B) by (conclude lemma_angleorderrespectscongruence2).

assert (CongA B E A A E B) by (conclude lemma_ABCequalsCBA).

assert (LtA B E f B E A) by (conclude lemma_angleorderrespectscongruence).

assert (Out E B B) by (conclude lemma_ray4).

assert (Out E A A) by (conclude lemma_ray4).

let Tf:=fresh in

assert (Tf:∃ m, (BetS A m B ∧ Out E f m)) by (conclude lemma_crossbar2);destruct Tf as [m];spliter.

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

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

assert (Cong M E A M) by (conclude lemma_congruencesymmetric).

assert (Cong E M A M) by (forward_using lemma_congruenceflip).

assert (Cong M B M Q) by (forward_using lemma_congruenceflip).

assert (nCol P A E) by (forward_using lemma_NCorder).

assert (Col P A Q) by (conclude_def Col ).

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

assert (Col P A A) by (conclude_def Col ).

assert (neq A Q) by (forward_using lemma_betweennotequal).

assert (neq Q A) by (conclude lemma_inequalitysymmetric).

assert (nCol Q A E) by (conclude lemma_NChelper).

assert (nCol E A Q) by (forward_using lemma_NCorder).

let Tf:=fresh in

assert (Tf:∃ F, (BetS E m F ∧ BetS Q A F)) by (conclude postulate_Euclid5);destruct Tf as [F];spliter.

assert (Col E m F) by (conclude_def Col ).

assert (Col m E F) by (forward_using lemma_collinearorder).

assert (Col E f m) by (conclude lemma_rayimpliescollinear).

assert (Col m E f) by (forward_using lemma_collinearorder).

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

assert (neq m E) by (conclude lemma_inequalitysymmetric).

assert (Col E f F) by (conclude lemma_collinear4).

assert (Col Q A F) by (conclude_def Col ).

assert (BetS Q A P) by (conclude axiom_betweennesssymmetry).

assert (Col Q A P) by (conclude_def Col ).

assert (neq Q A) by (forward_using lemma_betweennotequal).

assert (neq A Q) by (conclude lemma_inequalitysymmetric).

assert (Col A Q F) by (forward_using lemma_collinearorder).

assert (Col A Q P) by (forward_using lemma_collinearorder).

assert (Col Q F P) by (conclude lemma_collinear4).

assert (Col P Q F) by (forward_using lemma_collinearorder).

assert (neq E f) by (conclude lemma_ray2).

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

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

assert (Meet E f P Q) by (conclude_def Meet ).

contradict.

}

assert (¬ ¬ CongA C E A C E f).

{

intro.

assert (LtA C E A C E f) by (conclude lemma_angletrichotomy2).

contradict.

}

let Tf:=fresh in

assert (Tf:∃ a d p q, (Out E C d ∧ Out E A a ∧ Out E C p ∧ Out E f q ∧ Cong E d E p ∧ Cong E a E q ∧ Cong d a p q ∧ nCol C E A)) by (conclude_def CongA );destruct Tf as [a[d[p[q]]]];spliter.

assert (Col P Q A) by (conclude_def Col ).

assert (eq d p) by (conclude lemma_layoffunique).

assert (Cong d a d q) by (conclude cn_equalitysub).

assert (Cong a d q d) by (forward_using lemma_congruenceflip).

assert (Cong a E q E) by (forward_using lemma_congruenceflip).

assert (neq E d) by (conclude lemma_raystrict).

assert (Col E C d) by (conclude lemma_rayimpliescollinear).

assert (OS A f E d) by (conclude lemma_samesidecollinear).

assert (Col E d E) by (conclude_def Col ).

assert (Col E E d) by (forward_using lemma_collinearorder).

assert (OS A q E d) by (conclude lemma_sameside2).

assert (OS q A E d) by (forward_using lemma_samesidesymmetric).

assert (OS q a E d) by (conclude lemma_sameside2).

assert (OS a q E d) by (forward_using lemma_samesidesymmetric).

assert (eq a q) by (conclude proposition_07).

assert (Col E A a) by (conclude lemma_rayimpliescollinear).

assert (Col E f q) by (conclude lemma_rayimpliescollinear).

assert (Col E A q) by (conclude cn_equalitysub).

assert (Col q E A) by (forward_using lemma_collinearorder).

assert (Col q E f) by (forward_using lemma_collinearorder).

assert (neq E q) by (conclude lemma_raystrict).

assert (neq q E) by (conclude lemma_inequalitysymmetric).

assert (Col E A f) by (conclude lemma_collinear4).

assert (Col E f A) by (forward_using lemma_collinearorder).

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

assert (Meet E f P Q) by (conclude_def Meet ).

contradict.

}

let Tf:=fresh in

assert (Tf:∃ F, (neq E f ∧ neq P Q ∧ Col E f F ∧ Col P Q F)) by (conclude_def Meet );destruct Tf as [F];spliter.

assert (neq C E) by (conclude lemma_inequalitysymmetric).

assert (Par P Q E C) by (conclude lemma_collinearparallel).

assert (Par E C P Q) by (conclude lemma_parallelsymmetric).

let Tf:=fresh in

assert (Tf:∃ G, (PG F G C E ∧ Col P Q G)) by (conclude lemma_triangletoparallelogram);destruct Tf as [G];spliter.

assert (PG G F E C) by (conclude lemma_PGflip).

assert (PG F E C G) by (conclude lemma_PGrotate).

assert (Col P A Q) by (conclude_def Col ).

assert (Col P Q A) by (forward_using lemma_collinearorder).

assert (Par F E C G) by (conclude_def PG ).

assert (nCol F E G) by (forward_using lemma_parallelNC).

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

assert (Col F G A) by (conclude lemma_collinear5).

assert (ET F E C A E C) by (conclude proposition_41).

assert (Par P Q C B) by (forward_using lemma_parallelflip).

assert (Col C B E) by (forward_using lemma_collinearorder).

assert (neq E B) by (conclude lemma_inequalitysymmetric).

assert (Par P Q E B) by (conclude lemma_collinearparallel).

assert (Par P Q B E) by (forward_using lemma_parallelflip).

assert (Cong B E E C) by (forward_using lemma_congruenceflip).

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

assert (Col B E E) by (conclude_def Col ).

assert (ET A B E A E C) by (conclude proposition_38).

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

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

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

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

assert (Col A E E) by (conclude_def Col ).

assert (nCol A E B) by (forward_using lemma_NCorder).

assert (TS B A E C) by (conclude_def TS ).

assert (PG E F G C) by (conclude lemma_PGflip).

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

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

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

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

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

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

let Tf:=fresh in

assert (Tf:∃ m, (BetS E m G ∧ BetS F m C)) by (conclude lemma_diagonalsmeet);destruct Tf as [m];spliter.

assert (Col F m C) by (conclude_def Col ).

assert (Col F C m) by (forward_using lemma_collinearorder).

assert (Par F E C G) by (conclude_def PG ).

assert (nCol F E C) by (forward_using lemma_parallelNC).

assert (nCol F C E) by (forward_using lemma_NCorder).

assert (TS E F C G) by (conclude_def TS ).

assert (ET A E C F E C) by (conclude axiom_ETsymmetric).

assert (ET A E B F E C) by (conclude axiom_ETtransitive).

assert (ET A E B F C E) by (forward_using axiom_ETpermutation).

assert (ET A E C F E C) by (conclude axiom_ETsymmetric).

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

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

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

assert (ET A E C F C G) by (conclude axiom_ETtransitive).

assert (EF A B E C F E C G) by (conclude axiom_paste3).

assert (nCol F E C) by (forward_using lemma_parallelNC).

assert (nCol C E F) by (forward_using lemma_NCorder).

assert (CongA C E F C E F) by (conclude lemma_equalanglesreflexive).

assert ((eq E f ∨ eq E F ∨ eq f F ∨ BetS f E F ∨ BetS E f F ∨ BetS E F f)) by (conclude_def Col ).

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

assert (neq E F) by (conclude lemma_inequalitysymmetric).

assert (Out E F f).

by cases on (eq E f ∨ eq E F ∨ eq f F ∨ BetS f E F ∨ BetS E f F ∨ BetS E F f).

{

assert (¬ ¬ Out E F f).

{

intro.

contradict.

}

close.

}

{

assert (¬ ¬ Out E F f).

{

intro.

contradict.

}

close.

}

{

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

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

assert (Out E F f) by (conclude cn_equalitysub).

close.

}

{

assert (¬ ¬ Out E F f).

{

intro.

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

assert (Col E C E) by (conclude_def Col ).

assert (BetS F E f) by (conclude axiom_betweennesssymmetry).

assert (nCol E C F) by (forward_using lemma_NCorder).

assert (TS F E C f) by (conclude_def TS ).

assert (TS f E C F) by (conclude lemma_oppositesidesymmetric).

assert (OS A f E C) by (forward_using lemma_samesidesymmetric).

assert (TS A E C F) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ j, (BetS A j F ∧ Col E C j ∧ nCol E C A)) by (conclude_def TS );destruct Tf as [j];spliter.

assert (Col A j F) by (conclude_def Col ).

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

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

assert (Col Q A F) by (conclude lemma_collinear4).

assert (Col A F Q) by (forward_using lemma_collinearorder).

assert (Col Q P A) by (forward_using lemma_collinearorder).

assert (Col Q P F) by (forward_using lemma_collinearorder).

assert (Col P A F) by (conclude lemma_collinear4).

assert (Col A F P) by (forward_using lemma_collinearorder).

assert (Col A F j) by (forward_using lemma_collinearorder).

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

assert (neq A F) by (forward_using lemma_betweennotequal).

assert (Col P Q j) by (conclude lemma_collinear5).

assert (Meet P Q E C) by (conclude_def Meet ).

assert (¬ Meet P Q E C) by (conclude_def Par ).

contradict.

}

close.

}

{

assert (Out E F f) by (conclude lemma_ray4).

close.

}

{

assert (Out E F f) by (conclude lemma_ray4).

close.

}

assert (CongA C E F c E f) by (conclude lemma_equalangleshelper).

assert (CongA F E C f E c) by (conclude lemma_equalanglesflip).

assert (CongA F E C J D K) by (conclude lemma_equalanglestransitive).

assert (CongA C E F F E C) by (conclude lemma_ABCequalsCBA).

assert (CongA C E F J D K) by (conclude lemma_equalanglestransitive).

close.

Qed.

End Euclid.