# Library GeoCoq.Elements.OriginalProofs.proposition_27

Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglesflip.

Require Export GeoCoq.Elements.OriginalProofs.proposition_16.

Require Export GeoCoq.Elements.OriginalProofs.lemma_angletrichotomy.

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearbetween.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_27 :

∀ A B C D E F,

BetS A E B → BetS C F D → CongA A E F E F D → TS A E F D →

Par A B C D.

Proof.

intros.

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

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

rename_H H;let Tf:=fresh in

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

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

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

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

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

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

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

assert (CongA E F D A E F) by (conclude lemma_equalanglessymmetric).

assert (nCol E F D) by (conclude_def CongA ).

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

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

assert (¬ Meet A B C D).

{

intro.

let Tf:=fresh in

assert (Tf:∃ G, (neq A B ∧ neq C D ∧ Col A B G ∧ Col C D G)) by (conclude_def Meet );destruct Tf as [G];spliter.

assert (Col B A G) by (forward_using lemma_collinearorder).

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

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

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

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

assert (nCol A E F) by (conclude_def CongA ).

assert (¬ eq A E).

{

intro.

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

contradict.

}

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

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

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

assert (CongA E F D A E F) by (conclude lemma_equalanglessymmetric).

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

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

assert (BetS D F C) by (conclude axiom_betweennesssymmetry).

assert (Supp D F E E C) by (conclude_def Supp ).

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

assert (CongA A E F D F E) by (conclude lemma_equalanglestransitive).

assert (CongA F E B E F C) by (conclude lemma_supplements).

assert (CongA B E F C F E) by (conclude lemma_equalanglesflip).

assert (¬ BetS A E G).

{

intro.

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

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

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

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

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

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

assert (Col D G F) by (conclude lemma_collinear4).

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

assert (¬ eq F G).

{

intro.

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

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

contradict.

}

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

assert (¬ Col E F G).

{

intro.

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

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

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

contradict.

}

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

assert (OS D G E F) by (conclude_def OS ).

assert (OS G D E F) by (forward_using lemma_samesidesymmetric).

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

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

assert (BetS D F C) by (conclude axiom_betweennesssymmetry).

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

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

let Tf:=fresh in

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

assert (¬ neq F R).

{

intro.

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

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

assert (Col G R C) by (conclude_def Col ).

assert (Col C G D) by (forward_using lemma_collinearorder).

assert (Col C G R) by (forward_using lemma_collinearorder).

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

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

assert (Col G D R) by (conclude lemma_collinear4).

assert (Col G C R) by (forward_using lemma_collinearorder).

assert (Col G C D) by (forward_using lemma_collinearorder).

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

assert (Col C R D) by (conclude lemma_collinear4).

assert (Col C D R) by (forward_using lemma_collinearorder).

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

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

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

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

assert (Col C G R) by (forward_using lemma_collinearorder).

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

assert (Col D F G) by (conclude lemma_collinear4).

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

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

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

assert (Col F G C) by (conclude lemma_collinear4).

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

assert (Col C G D) by (forward_using lemma_collinearorder).

assert (Col R F D) by (conclude lemma_collinear5).

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

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

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

contradict.

}

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

assert (¬ Col E G F).

{

intro.

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

contradict.

}

assert (Triangle E G F) by (conclude_def Triangle ).

assert (LtA G E F E F C) by (conclude proposition_16).

assert (LtA G E F F E B) by (conclude lemma_angleorderrespectscongruence).

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

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

assert (Out E G B) by (conclude_def Out ).

assert (¬ Col G E F).

{

intro.

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

contradict.

}

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

assert (CongA G E F B E F) by (conclude lemma_equalangleshelper).

assert (nCol B E F) by (conclude_def CongA ).

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

assert (CongA G E F F E B) by (conclude lemma_equalanglestransitive).

assert (CongA F E B G E F) by (conclude lemma_equalanglessymmetric).

assert (LtA F E B F E B) by (conclude lemma_angleorderrespectscongruence2).

assert (¬ LtA F E B F E B) by (conclude lemma_angletrichotomy).

contradict.

}

assert (¬ Out E A G).

{

intro.

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

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

assert (Out E G A) by (conclude lemma_ray5).

assert (CongA E F D A E F) by (conclude lemma_equalanglessymmetric).

assert (CongA E F D G E F) by (conclude lemma_equalangleshelper).

assert (CongA G E F E F D) by (conclude lemma_equalanglessymmetric).

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

assert ((BetS E A G ∨ eq G A ∨ BetS E G A)) by (conclude lemma_ray1).

assert (BetS B E G).

by cases on (BetS E A G ∨ eq G A ∨ BetS E G A).

{

assert (BetS B E G) by (conclude lemma_3_7b).

close.

}

{

assert (BetS B E G) by (conclude cn_equalitysub).

close.

}

{

assert (BetS B E G) by (conclude axiom_innertransitivity).

close.

}

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

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

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

assert (¬ Col E F G).

{

intro.

assert (Col B A G) by (forward_using lemma_collinearorder).

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

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

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

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

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

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

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

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

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

contradict.

}

assert (OS A G E F) by (conclude_def OS ).

assert (OS G A E F) by (forward_using lemma_samesidesymmetric).

assert (TS G E F D) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ P, (BetS G P D ∧ Col E F P ∧ nCol E F G)) by (conclude_def TS );destruct Tf as [P];spliter.

assert (Col G P D) by (conclude_def Col ).

assert (¬ neq P F).

{

intro.

assert (neq G D) by (forward_using lemma_betweennotequal).

assert (Col G D P) by (forward_using lemma_collinearorder).

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

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

assert (Col D G F) by (conclude lemma_collinear4).

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

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

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

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

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

assert (¬ Col F D E).

{

intro.

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

contradict.

}

contradict.

}

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

assert (¬ Col F E A).

{

intro.

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

contradict.

}

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

assert (CongA F E A F E G) by (conclude lemma_equalangleshelper).

assert (CongA F E G F E A) by (conclude lemma_equalanglessymmetric).

assert (nCol F E G) by (conclude_def CongA ).

assert (¬ Col E G F).

{

intro.

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

contradict.

}

assert (Triangle E G F) by (conclude_def Triangle ).

assert (LtA G E F E F D) by (conclude proposition_16).

assert (LtA E F D E F D) by (conclude lemma_angleorderrespectscongruence2).

assert (¬ LtA E F D E F D) by (conclude lemma_angletrichotomy).

contradict.

}

assert ((eq A E ∨ eq A G ∨ eq E G ∨ BetS E A G ∨ BetS A E G ∨ BetS A G E)) by (conclude_def Col ).

assert (¬ Meet A B C D).

by cases on (eq A E ∨ eq A G ∨ eq E G ∨ BetS E A G ∨ BetS A E G ∨ BetS A G E).

{

assert (¬ Meet A B C D).

{

intro.

contradict.

}

close.

}

{

assert (¬ Col A F E).

{

intro.

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

contradict.

}

assert (Triangle A F E) by (conclude_def Triangle ).

assert (¬ neq H F).

{

intro.

assert (Col C D A) by (conclude cn_equalitysub).

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

assert (Col D G F) by (conclude lemma_collinear4).

assert (Col D A F) by (conclude cn_equalitysub).

assert (Col A H D) by (conclude_def Col ).

assert (Col D A H) by (forward_using lemma_collinearorder).

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

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

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

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

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

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

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

contradict.

}

assert (BetS A F D) by (conclude cn_equalitysub).

assert (¬ Col E A F).

{

intro.

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

contradict.

}

assert (Triangle E A F) by (conclude_def Triangle ).

assert (LtA A E F E F D) by (conclude proposition_16).

assert (CongA E F D A E F) by (conclude lemma_equalanglessymmetric).

assert (LtA E F D E F D) by (conclude lemma_angleorderrespectscongruence2).

assert (¬ Meet A B C D).

{

intro.

assert (¬ LtA E F D E F D) by (conclude lemma_angletrichotomy).

contradict.

}

close.

}

{

assert (Col C D E) by (conclude cn_equalitysub).

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

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

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

assert (¬ neq E F).

{

intro.

assert (Col F D H) by (conclude lemma_collinear4).

assert (Col D H F) by (forward_using lemma_collinearorder).

assert (Col A H D) by (conclude_def Col ).

assert (Col D H A) by (forward_using lemma_collinearorder).

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

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

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

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

assert (¬ neq H F).

{

intro.

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

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

contradict.

}

assert (Col A H D) by (conclude_def Col ).

assert (Col A F D) by (conclude cn_equalitysub).

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

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

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

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

assert (neq D F) by (conclude cn_equalitysub).

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

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

assert (Col D C G) by (forward_using lemma_collinearorder).

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

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

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

assert (Col C G F) by (conclude lemma_collinear4).

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

assert (¬ neq C F).

{

intro.

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

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

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

contradict.

}

assert (Col C D E) by (conclude cn_equalitysub).

assert (eq C H) by (conclude cn_equalitytransitive).

assert (Col A H D) by (conclude_def Col ).

assert (Col A C D) by (conclude cn_equalitysub).

assert (Col C D A) by (forward_using lemma_collinearorder).

assert (Col F D A) by (conclude cn_equalitysub).

assert (Col C D E) by (conclude cn_equalitysub).

assert (Col F D E) by (conclude cn_equalitysub).

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

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

assert (neq D F) by (conclude cn_equalitysub).

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

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

contradict.

}

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

assert (¬ Meet A B C D).

{

intro.

contradict.

}

close.

}

{

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

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

assert (¬ Meet A B C D).

{

intro.

contradict.

}

close.

}

{

assert (¬ Meet A B C D).

{

intro.

contradict.

}

close.

}

{

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

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

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

assert (¬ Meet A B C D).

{

intro.

contradict.

}

close.

}

contradict.

}

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

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

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

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

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

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

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

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

assert (BetS E H F) by (conclude lemma_collinearbetween).

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

assert (Par A B C D) by (conclude_def Par ).

close.

Unshelve.

apply B.

Qed.

End Euclid.

Require Export GeoCoq.Elements.OriginalProofs.proposition_16.

Require Export GeoCoq.Elements.OriginalProofs.lemma_angletrichotomy.

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearbetween.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_27 :

∀ A B C D E F,

BetS A E B → BetS C F D → CongA A E F E F D → TS A E F D →

Par A B C D.

Proof.

intros.

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

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

rename_H H;let Tf:=fresh in

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

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

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

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

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

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

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

assert (CongA E F D A E F) by (conclude lemma_equalanglessymmetric).

assert (nCol E F D) by (conclude_def CongA ).

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

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

assert (¬ Meet A B C D).

{

intro.

let Tf:=fresh in

assert (Tf:∃ G, (neq A B ∧ neq C D ∧ Col A B G ∧ Col C D G)) by (conclude_def Meet );destruct Tf as [G];spliter.

assert (Col B A G) by (forward_using lemma_collinearorder).

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

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

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

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

assert (nCol A E F) by (conclude_def CongA ).

assert (¬ eq A E).

{

intro.

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

contradict.

}

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

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

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

assert (CongA E F D A E F) by (conclude lemma_equalanglessymmetric).

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

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

assert (BetS D F C) by (conclude axiom_betweennesssymmetry).

assert (Supp D F E E C) by (conclude_def Supp ).

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

assert (CongA A E F D F E) by (conclude lemma_equalanglestransitive).

assert (CongA F E B E F C) by (conclude lemma_supplements).

assert (CongA B E F C F E) by (conclude lemma_equalanglesflip).

assert (¬ BetS A E G).

{

intro.

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

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

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

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

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

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

assert (Col D G F) by (conclude lemma_collinear4).

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

assert (¬ eq F G).

{

intro.

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

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

contradict.

}

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

assert (¬ Col E F G).

{

intro.

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

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

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

contradict.

}

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

assert (OS D G E F) by (conclude_def OS ).

assert (OS G D E F) by (forward_using lemma_samesidesymmetric).

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

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

assert (BetS D F C) by (conclude axiom_betweennesssymmetry).

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

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

let Tf:=fresh in

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

assert (¬ neq F R).

{

intro.

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

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

assert (Col G R C) by (conclude_def Col ).

assert (Col C G D) by (forward_using lemma_collinearorder).

assert (Col C G R) by (forward_using lemma_collinearorder).

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

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

assert (Col G D R) by (conclude lemma_collinear4).

assert (Col G C R) by (forward_using lemma_collinearorder).

assert (Col G C D) by (forward_using lemma_collinearorder).

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

assert (Col C R D) by (conclude lemma_collinear4).

assert (Col C D R) by (forward_using lemma_collinearorder).

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

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

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

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

assert (Col C G R) by (forward_using lemma_collinearorder).

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

assert (Col D F G) by (conclude lemma_collinear4).

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

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

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

assert (Col F G C) by (conclude lemma_collinear4).

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

assert (Col C G D) by (forward_using lemma_collinearorder).

assert (Col R F D) by (conclude lemma_collinear5).

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

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

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

contradict.

}

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

assert (¬ Col E G F).

{

intro.

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

contradict.

}

assert (Triangle E G F) by (conclude_def Triangle ).

assert (LtA G E F E F C) by (conclude proposition_16).

assert (LtA G E F F E B) by (conclude lemma_angleorderrespectscongruence).

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

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

assert (Out E G B) by (conclude_def Out ).

assert (¬ Col G E F).

{

intro.

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

contradict.

}

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

assert (CongA G E F B E F) by (conclude lemma_equalangleshelper).

assert (nCol B E F) by (conclude_def CongA ).

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

assert (CongA G E F F E B) by (conclude lemma_equalanglestransitive).

assert (CongA F E B G E F) by (conclude lemma_equalanglessymmetric).

assert (LtA F E B F E B) by (conclude lemma_angleorderrespectscongruence2).

assert (¬ LtA F E B F E B) by (conclude lemma_angletrichotomy).

contradict.

}

assert (¬ Out E A G).

{

intro.

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

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

assert (Out E G A) by (conclude lemma_ray5).

assert (CongA E F D A E F) by (conclude lemma_equalanglessymmetric).

assert (CongA E F D G E F) by (conclude lemma_equalangleshelper).

assert (CongA G E F E F D) by (conclude lemma_equalanglessymmetric).

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

assert ((BetS E A G ∨ eq G A ∨ BetS E G A)) by (conclude lemma_ray1).

assert (BetS B E G).

by cases on (BetS E A G ∨ eq G A ∨ BetS E G A).

{

assert (BetS B E G) by (conclude lemma_3_7b).

close.

}

{

assert (BetS B E G) by (conclude cn_equalitysub).

close.

}

{

assert (BetS B E G) by (conclude axiom_innertransitivity).

close.

}

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

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

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

assert (¬ Col E F G).

{

intro.

assert (Col B A G) by (forward_using lemma_collinearorder).

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

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

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

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

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

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

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

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

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

contradict.

}

assert (OS A G E F) by (conclude_def OS ).

assert (OS G A E F) by (forward_using lemma_samesidesymmetric).

assert (TS G E F D) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ P, (BetS G P D ∧ Col E F P ∧ nCol E F G)) by (conclude_def TS );destruct Tf as [P];spliter.

assert (Col G P D) by (conclude_def Col ).

assert (¬ neq P F).

{

intro.

assert (neq G D) by (forward_using lemma_betweennotequal).

assert (Col G D P) by (forward_using lemma_collinearorder).

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

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

assert (Col D G F) by (conclude lemma_collinear4).

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

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

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

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

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

assert (¬ Col F D E).

{

intro.

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

contradict.

}

contradict.

}

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

assert (¬ Col F E A).

{

intro.

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

contradict.

}

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

assert (CongA F E A F E G) by (conclude lemma_equalangleshelper).

assert (CongA F E G F E A) by (conclude lemma_equalanglessymmetric).

assert (nCol F E G) by (conclude_def CongA ).

assert (¬ Col E G F).

{

intro.

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

contradict.

}

assert (Triangle E G F) by (conclude_def Triangle ).

assert (LtA G E F E F D) by (conclude proposition_16).

assert (LtA E F D E F D) by (conclude lemma_angleorderrespectscongruence2).

assert (¬ LtA E F D E F D) by (conclude lemma_angletrichotomy).

contradict.

}

assert ((eq A E ∨ eq A G ∨ eq E G ∨ BetS E A G ∨ BetS A E G ∨ BetS A G E)) by (conclude_def Col ).

assert (¬ Meet A B C D).

by cases on (eq A E ∨ eq A G ∨ eq E G ∨ BetS E A G ∨ BetS A E G ∨ BetS A G E).

{

assert (¬ Meet A B C D).

{

intro.

contradict.

}

close.

}

{

assert (¬ Col A F E).

{

intro.

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

contradict.

}

assert (Triangle A F E) by (conclude_def Triangle ).

assert (¬ neq H F).

{

intro.

assert (Col C D A) by (conclude cn_equalitysub).

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

assert (Col D G F) by (conclude lemma_collinear4).

assert (Col D A F) by (conclude cn_equalitysub).

assert (Col A H D) by (conclude_def Col ).

assert (Col D A H) by (forward_using lemma_collinearorder).

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

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

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

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

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

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

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

contradict.

}

assert (BetS A F D) by (conclude cn_equalitysub).

assert (¬ Col E A F).

{

intro.

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

contradict.

}

assert (Triangle E A F) by (conclude_def Triangle ).

assert (LtA A E F E F D) by (conclude proposition_16).

assert (CongA E F D A E F) by (conclude lemma_equalanglessymmetric).

assert (LtA E F D E F D) by (conclude lemma_angleorderrespectscongruence2).

assert (¬ Meet A B C D).

{

intro.

assert (¬ LtA E F D E F D) by (conclude lemma_angletrichotomy).

contradict.

}

close.

}

{

assert (Col C D E) by (conclude cn_equalitysub).

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

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

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

assert (¬ neq E F).

{

intro.

assert (Col F D H) by (conclude lemma_collinear4).

assert (Col D H F) by (forward_using lemma_collinearorder).

assert (Col A H D) by (conclude_def Col ).

assert (Col D H A) by (forward_using lemma_collinearorder).

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

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

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

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

assert (¬ neq H F).

{

intro.

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

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

contradict.

}

assert (Col A H D) by (conclude_def Col ).

assert (Col A F D) by (conclude cn_equalitysub).

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

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

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

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

assert (neq D F) by (conclude cn_equalitysub).

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

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

assert (Col D C G) by (forward_using lemma_collinearorder).

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

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

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

assert (Col C G F) by (conclude lemma_collinear4).

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

assert (¬ neq C F).

{

intro.

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

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

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

contradict.

}

assert (Col C D E) by (conclude cn_equalitysub).

assert (eq C H) by (conclude cn_equalitytransitive).

assert (Col A H D) by (conclude_def Col ).

assert (Col A C D) by (conclude cn_equalitysub).

assert (Col C D A) by (forward_using lemma_collinearorder).

assert (Col F D A) by (conclude cn_equalitysub).

assert (Col C D E) by (conclude cn_equalitysub).

assert (Col F D E) by (conclude cn_equalitysub).

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

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

assert (neq D F) by (conclude cn_equalitysub).

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

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

contradict.

}

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

assert (¬ Meet A B C D).

{

intro.

contradict.

}

close.

}

{

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

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

assert (¬ Meet A B C D).

{

intro.

contradict.

}

close.

}

{

assert (¬ Meet A B C D).

{

intro.

contradict.

}

close.

}

{

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

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

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

assert (¬ Meet A B C D).

{

intro.

contradict.

}

close.

}

contradict.

}

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

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

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

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

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

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

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

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

assert (BetS E H F) by (conclude lemma_collinearbetween).

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

assert (Par A B C D) by (conclude_def Par ).

close.

Unshelve.

apply B.

Qed.

End Euclid.