# Library GeoCoq.Elements.OriginalProofs.lemma_angletrichotomy2

Require Export GeoCoq.Elements.OriginalProofs.proposition_23C.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_angletrichotomy2 :

∀ A B C D E F,

nCol A B C → nCol D E F → ¬ CongA A B C D E F → ¬ LtA D E F A B C →

LtA A B C D E F.

Proof.

intros.

assert (¬ eq B A).

{

intro.

assert (eq A B) by (conclude lemma_equalitysymmetric).

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

contradict.

}

assert (¬ eq B C).

{

intro.

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

contradict.

}

assert (¬ Col B A C).

{

intro.

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

contradict.

}

let Tf:=fresh in

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

assert (nCol B A G) by (conclude_def OS ).

assert (¬ eq B G).

{

intro.

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

contradict.

}

assert (¬ eq A G).

{

intro.

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

contradict.

}

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

assert (Out B J A) by (conclude lemma_ray5).

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

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

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

assert (nCol G B A) by (conclude lemma_equalanglesNC).

assert (¬ Col A B G).

{

intro.

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

contradict.

}

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

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

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

assert (¬ Col A B G).

{

intro.

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

contradict.

}

assert (¬ eq G A).

{

intro.

assert (eq A G) by (conclude lemma_equalitysymmetric).

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

contradict.

}

let Tf:=fresh in

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

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

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

assert (¬ Col B A G).

{

intro.

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

contradict.

}

assert (OS C G B A) by (forward_using lemma_samesidesymmetric).

assert (TS G B A P) by (conclude_def TS ).

assert (TS C B A P) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ R, (BetS C R P ∧ Col B A R ∧ nCol B A C)) by (conclude_def TS );destruct Tf as [R];spliter.

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

assert (LtA A B C D E F).

by cases on (TS G B C A ∨ ¬ TS G B C A).

{

rename_H H;let Tf:=fresh in

assert (Tf:∃ H, (BetS G H A ∧ Col B C H ∧ nCol B C G)) by (conclude_def TS );destruct Tf as [H];spliter.

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

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

assert (¬ Col A B H).

{

intro.

assert (¬ eq B H).

{

intro.

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

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

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

contradict.

}

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

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

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

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

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

contradict.

}

assert (CongA A B H A B H) by (conclude lemma_equalanglesreflexive).

assert (LtA A B H A B G) by (conclude_def LtA ).

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

assert (LtA A B H G B A) by (conclude lemma_angleorderrespectscongruence).

assert (¬ Col H B A).

{

intro.

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

contradict.

}

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

assert (LtA H B A G B A) by (conclude lemma_angleorderrespectscongruence2).

assert (LtA H B A D E F) by (conclude lemma_angleorderrespectscongruence).

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

assert (LtA A B H D E F) by (conclude lemma_angleorderrespectscongruence2).

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

assert (OS C G B A) by (forward_using lemma_samesidesymmetric).

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

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

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

assert (OS C H B A) by (conclude lemma_sameside2).

assert (¬ BetS C B H).

{

intro.

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

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

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

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

assert (TS C B A C) by (conclude lemma_planeseparation).

let Tf:=fresh in

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

assert (¬ BetS C M C) by (conclude axiom_betweennessidentity).

contradict.

}

assert ((eq B C ∨ eq B H ∨ eq C H ∨ BetS C B H ∨ BetS B C H ∨ BetS B H C)) by (conclude_def Col ).

assert (Out B C H).

by cases on (eq B C ∨ eq B H ∨ eq C H ∨ BetS C B H ∨ BetS B C H ∨ BetS B H C).

{

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

assert (¬ ¬ Out B C H).

{

intro.

contradict.

}

close.

}

{

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

assert (¬ ¬ Out B C H).

{

intro.

assert (¬ Col B H A).

{

intro.

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

contradict.

}

contradict.

}

close.

}

{

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

assert (Out B C H).

by cases on (eq B H ∨ neq B H).

{

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

assert (¬ ¬ Out B C H).

{

intro.

assert (¬ Col B H A).

{

intro.

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

contradict.

}

contradict.

}

close.

}

{

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

assert (Out B C H) by (conclude cn_equalitysub).

close.

}

close.

}

{

assert (¬ ¬ Out B C H).

{

intro.

contradict.

}

close.

}

{

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

assert (Out B C H) by (conclude lemma_ray4).

close.

}

{

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

assert (Out B C H) by (conclude lemma_ray4).

close.

}

assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).

assert (CongA A B C A B H) by (conclude lemma_equalangleshelper).

assert (LtA A B C D E F) by (conclude lemma_angleorderrespectscongruence2).

close.

}

{

assert ((eq B A ∨ eq B R ∨ eq A R ∨ BetS A B R ∨ BetS B A R ∨ BetS B R A)) by (conclude_def Col ).

assert (LtA A B C D E F).

by cases on (eq B A ∨ eq B R ∨ eq A R ∨ BetS A B R ∨ BetS B A R ∨ BetS B R A).

{

assert (¬ ¬ LtA A B C D E F).

{

intro.

contradict.

}

close.

}

{

assert (eq R B) by (conclude lemma_equalitysymmetric).

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

assert (¬ Col C P G).

{

intro.

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

assert (Col C B P) by (conclude cn_equalitysub).

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

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

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

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

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

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

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

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

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

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ Q, (BetS C Q A ∧ BetS G Q R)) by (conclude postulate_Pasch_inner);destruct Tf as [Q];spliter.

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

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

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

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

assert (Out B Q G) by (conclude lemma_ray4).

assert (Out B G Q) by (conclude lemma_ray5).

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

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

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

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

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

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

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

assert (Cong A Q A Q) by (conclude cn_congruencereflexive).

assert (Cong B Q B Q) by (conclude cn_congruencereflexive).

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (CongA A B G A B Q) by (conclude_def CongA ).

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

assert (LtA A B G A B C) by (conclude_def LtA ).

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

assert (LtA D E F A B C) by (conclude lemma_angleorderrespectscongruence2).

assert (¬ ¬ LtA A B C D E F).

{

intro.

contradict.

}

close.

}

{

assert (¬ ¬ LtA A B C D E F).

{

intro.

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

assert (BetS P A C) by (conclude cn_equalitysub).

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

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

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

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

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

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

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

assert (¬ BetS A G C).

{

intro.

assert (CongA A B G A B G) by (conclude lemma_equalanglesreflexive).

assert (LtA A B G A B C) by (conclude_def LtA ).

assert (LtA D E F A B C) by (conclude lemma_angleorderrespectscongruence2).

contradict.

}

assert (¬ BetS A C G).

{

intro.

assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).

assert (LtA A B C A B G) by (conclude_def LtA ).

assert (LtA A B C D E F) by (conclude lemma_angleorderrespectscongruence).

contradict.

}

assert (eq C G) by (conclude lemma_outerconnectivity).

assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).

assert (CongA A B G A B C) by (conclude cn_equalitysub).

assert (CongA A B C A B G) by (conclude lemma_equalanglessymmetric).

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

contradict.

}

close.

}

{

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

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

assert (¬ Col C P A).

{

intro.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ M, (BetS A M P ∧ BetS C B M)) by (conclude postulate_Pasch_outer);destruct Tf as [M];spliter.

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

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

assert (BetS M A G) by (conclude lemma_3_6a).

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

assert (¬ Col C M G).

{

intro.

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

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

assert (BetS P M G) by (conclude lemma_3_6b).

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

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

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

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

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

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

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

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

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

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

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ Q, (BetS C Q A ∧ BetS G Q B)) by (conclude postulate_Pasch_inner);destruct Tf as [Q];spliter.

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

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

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

assert (Out B Q G) by (conclude lemma_ray4).

assert (Out B G Q) by (conclude lemma_ray5).

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

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

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

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

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

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

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

assert (Cong A Q A Q) by (conclude cn_congruencereflexive).

assert (Cong B Q B Q) by (conclude cn_congruencereflexive).

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (CongA A B G A B Q) by (conclude_def CongA ).

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

assert (LtA A B G A B C) by (conclude_def LtA ).

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

assert (LtA D E F A B C) by (conclude lemma_angleorderrespectscongruence2).

assert (¬ ¬ LtA A B C D E F).

{

intro.

contradict.

}

close.

}

{

assert (¬ Col P C B).

{

intro.

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

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

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

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

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

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

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

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

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

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

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ Q, (BetS B Q C ∧ BetS P A Q)) by (conclude postulate_Pasch_outer);destruct Tf as [Q];spliter.

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

assert (¬ eq G Q).

{

intro.

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

assert (Out B C G) by (conclude lemma_ray4).

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

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

assert (Cong A G A G) by (conclude cn_congruencereflexive).

assert (Cong B G B G) by (conclude cn_congruencereflexive).

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (CongA A B G A B C) by (conclude_def CongA ).

assert (CongA A B C A B G) by (conclude lemma_equalanglessymmetric).

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

contradict.

}

assert (¬ Col B C G).

{

intro.

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

assert (Out A G Q) by (conclude_def Out ).

assert (Col A G Q) by (conclude lemma_rayimpliescollinear).

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

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

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

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

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

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

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

assert (Col G Q B) by (conclude lemma_collinear5).

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

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

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

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

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

contradict.

}

assert (¬ BetS A Q G).

{

intro.

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

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

contradict.

}

assert (Out B C Q) by (conclude lemma_ray4).

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

assert (¬ BetS A G Q).

{

intro.

assert (CongA A B G A B G) by (conclude lemma_equalanglesreflexive).

assert (LtA A B G A B C) by (conclude_def LtA ).

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

assert (LtA D E F A B C) by (conclude lemma_angleorderrespectscongruence2).

contradict.

}

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

assert (eq G Q) by (conclude lemma_outerconnectivity).

assert (¬ ¬ LtA A B C D E F).

{

intro.

contradict.

}

close.

}

{

assert (¬ ¬ LtA A B C D E F).

{

intro.

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

assert (¬ Col P G B).

{

intro.

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

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

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

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

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ Q, (BetS B Q G ∧ BetS P R Q)) by (conclude postulate_Pasch_outer);destruct Tf as [Q];spliter.

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

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

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

assert (Out B G Q) by (conclude lemma_ray4).

assert (Out B Q G) by (conclude lemma_ray4).

assert (¬ BetS R C Q).

{

intro.

assert (Out B A R) by (conclude lemma_ray4).

assert (Out B G Q) by (conclude lemma_ray4).

assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).

assert (LtA A B C A B G) by (conclude_def LtA ).

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

assert (LtA A B C D E F) by (conclude lemma_angleorderrespectscongruence).

contradict.

}

assert (¬ BetS R Q C).

{

intro.

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

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

assert (Out B Q G) by (conclude lemma_ray4).

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

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

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (Cong B G B G) by (conclude cn_congruencereflexive).

assert (Cong A G A G) by (conclude cn_congruencereflexive).

assert (CongA A B G A B Q) by (conclude_def CongA ).

assert (Out B A R) by (conclude lemma_ray4).

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

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

assert (LtA A B G A B C) by (conclude_def LtA ).

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

assert (LtA D E F A B C) by (conclude lemma_angleorderrespectscongruence2).

contradict.

}

assert (eq Q C) by (conclude lemma_outerconnectivity).

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

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

assert (Out B C G) by (conclude cn_equalitysub).

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

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

assert (Out B Q G) by (conclude lemma_ray4).

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

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

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (Cong B G B G) by (conclude cn_congruencereflexive).

assert (Cong A G A G) by (conclude cn_congruencereflexive).

assert (CongA A B G A B Q) by (conclude_def CongA ).

assert (CongA A B C A B G) by (conclude_def CongA ).

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

contradict.

}

close.

}

close.

}

close.

Qed.

End Euclid.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_angletrichotomy2 :

∀ A B C D E F,

nCol A B C → nCol D E F → ¬ CongA A B C D E F → ¬ LtA D E F A B C →

LtA A B C D E F.

Proof.

intros.

assert (¬ eq B A).

{

intro.

assert (eq A B) by (conclude lemma_equalitysymmetric).

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

contradict.

}

assert (¬ eq B C).

{

intro.

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

contradict.

}

assert (¬ Col B A C).

{

intro.

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

contradict.

}

let Tf:=fresh in

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

assert (nCol B A G) by (conclude_def OS ).

assert (¬ eq B G).

{

intro.

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

contradict.

}

assert (¬ eq A G).

{

intro.

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

contradict.

}

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

assert (Out B J A) by (conclude lemma_ray5).

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

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

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

assert (nCol G B A) by (conclude lemma_equalanglesNC).

assert (¬ Col A B G).

{

intro.

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

contradict.

}

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

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

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

assert (¬ Col A B G).

{

intro.

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

contradict.

}

assert (¬ eq G A).

{

intro.

assert (eq A G) by (conclude lemma_equalitysymmetric).

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

contradict.

}

let Tf:=fresh in

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

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

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

assert (¬ Col B A G).

{

intro.

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

contradict.

}

assert (OS C G B A) by (forward_using lemma_samesidesymmetric).

assert (TS G B A P) by (conclude_def TS ).

assert (TS C B A P) by (conclude lemma_planeseparation).

let Tf:=fresh in

assert (Tf:∃ R, (BetS C R P ∧ Col B A R ∧ nCol B A C)) by (conclude_def TS );destruct Tf as [R];spliter.

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

assert (LtA A B C D E F).

by cases on (TS G B C A ∨ ¬ TS G B C A).

{

rename_H H;let Tf:=fresh in

assert (Tf:∃ H, (BetS G H A ∧ Col B C H ∧ nCol B C G)) by (conclude_def TS );destruct Tf as [H];spliter.

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

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

assert (¬ Col A B H).

{

intro.

assert (¬ eq B H).

{

intro.

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

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

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

contradict.

}

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

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

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

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

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

contradict.

}

assert (CongA A B H A B H) by (conclude lemma_equalanglesreflexive).

assert (LtA A B H A B G) by (conclude_def LtA ).

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

assert (LtA A B H G B A) by (conclude lemma_angleorderrespectscongruence).

assert (¬ Col H B A).

{

intro.

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

contradict.

}

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

assert (LtA H B A G B A) by (conclude lemma_angleorderrespectscongruence2).

assert (LtA H B A D E F) by (conclude lemma_angleorderrespectscongruence).

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

assert (LtA A B H D E F) by (conclude lemma_angleorderrespectscongruence2).

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

assert (OS C G B A) by (forward_using lemma_samesidesymmetric).

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

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

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

assert (OS C H B A) by (conclude lemma_sameside2).

assert (¬ BetS C B H).

{

intro.

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

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

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

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

assert (TS C B A C) by (conclude lemma_planeseparation).

let Tf:=fresh in

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

assert (¬ BetS C M C) by (conclude axiom_betweennessidentity).

contradict.

}

assert ((eq B C ∨ eq B H ∨ eq C H ∨ BetS C B H ∨ BetS B C H ∨ BetS B H C)) by (conclude_def Col ).

assert (Out B C H).

by cases on (eq B C ∨ eq B H ∨ eq C H ∨ BetS C B H ∨ BetS B C H ∨ BetS B H C).

{

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

assert (¬ ¬ Out B C H).

{

intro.

contradict.

}

close.

}

{

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

assert (¬ ¬ Out B C H).

{

intro.

assert (¬ Col B H A).

{

intro.

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

contradict.

}

contradict.

}

close.

}

{

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

assert (Out B C H).

by cases on (eq B H ∨ neq B H).

{

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

assert (¬ ¬ Out B C H).

{

intro.

assert (¬ Col B H A).

{

intro.

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

contradict.

}

contradict.

}

close.

}

{

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

assert (Out B C H) by (conclude cn_equalitysub).

close.

}

close.

}

{

assert (¬ ¬ Out B C H).

{

intro.

contradict.

}

close.

}

{

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

assert (Out B C H) by (conclude lemma_ray4).

close.

}

{

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

assert (Out B C H) by (conclude lemma_ray4).

close.

}

assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).

assert (CongA A B C A B H) by (conclude lemma_equalangleshelper).

assert (LtA A B C D E F) by (conclude lemma_angleorderrespectscongruence2).

close.

}

{

assert ((eq B A ∨ eq B R ∨ eq A R ∨ BetS A B R ∨ BetS B A R ∨ BetS B R A)) by (conclude_def Col ).

assert (LtA A B C D E F).

by cases on (eq B A ∨ eq B R ∨ eq A R ∨ BetS A B R ∨ BetS B A R ∨ BetS B R A).

{

assert (¬ ¬ LtA A B C D E F).

{

intro.

contradict.

}

close.

}

{

assert (eq R B) by (conclude lemma_equalitysymmetric).

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

assert (¬ Col C P G).

{

intro.

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

assert (Col C B P) by (conclude cn_equalitysub).

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

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

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

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

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

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

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

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

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

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ Q, (BetS C Q A ∧ BetS G Q R)) by (conclude postulate_Pasch_inner);destruct Tf as [Q];spliter.

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

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

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

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

assert (Out B Q G) by (conclude lemma_ray4).

assert (Out B G Q) by (conclude lemma_ray5).

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

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

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

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

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

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

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

assert (Cong A Q A Q) by (conclude cn_congruencereflexive).

assert (Cong B Q B Q) by (conclude cn_congruencereflexive).

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (CongA A B G A B Q) by (conclude_def CongA ).

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

assert (LtA A B G A B C) by (conclude_def LtA ).

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

assert (LtA D E F A B C) by (conclude lemma_angleorderrespectscongruence2).

assert (¬ ¬ LtA A B C D E F).

{

intro.

contradict.

}

close.

}

{

assert (¬ ¬ LtA A B C D E F).

{

intro.

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

assert (BetS P A C) by (conclude cn_equalitysub).

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

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

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

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

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

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

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

assert (¬ BetS A G C).

{

intro.

assert (CongA A B G A B G) by (conclude lemma_equalanglesreflexive).

assert (LtA A B G A B C) by (conclude_def LtA ).

assert (LtA D E F A B C) by (conclude lemma_angleorderrespectscongruence2).

contradict.

}

assert (¬ BetS A C G).

{

intro.

assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).

assert (LtA A B C A B G) by (conclude_def LtA ).

assert (LtA A B C D E F) by (conclude lemma_angleorderrespectscongruence).

contradict.

}

assert (eq C G) by (conclude lemma_outerconnectivity).

assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).

assert (CongA A B G A B C) by (conclude cn_equalitysub).

assert (CongA A B C A B G) by (conclude lemma_equalanglessymmetric).

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

contradict.

}

close.

}

{

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

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

assert (¬ Col C P A).

{

intro.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ M, (BetS A M P ∧ BetS C B M)) by (conclude postulate_Pasch_outer);destruct Tf as [M];spliter.

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

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

assert (BetS M A G) by (conclude lemma_3_6a).

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

assert (¬ Col C M G).

{

intro.

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

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

assert (BetS P M G) by (conclude lemma_3_6b).

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

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

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

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

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

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

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

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

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

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

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ Q, (BetS C Q A ∧ BetS G Q B)) by (conclude postulate_Pasch_inner);destruct Tf as [Q];spliter.

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

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

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

assert (Out B Q G) by (conclude lemma_ray4).

assert (Out B G Q) by (conclude lemma_ray5).

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

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

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

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

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

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

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

assert (Cong A Q A Q) by (conclude cn_congruencereflexive).

assert (Cong B Q B Q) by (conclude cn_congruencereflexive).

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (CongA A B G A B Q) by (conclude_def CongA ).

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

assert (LtA A B G A B C) by (conclude_def LtA ).

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

assert (LtA D E F A B C) by (conclude lemma_angleorderrespectscongruence2).

assert (¬ ¬ LtA A B C D E F).

{

intro.

contradict.

}

close.

}

{

assert (¬ Col P C B).

{

intro.

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

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

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

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

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

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

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

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

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

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

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ Q, (BetS B Q C ∧ BetS P A Q)) by (conclude postulate_Pasch_outer);destruct Tf as [Q];spliter.

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

assert (¬ eq G Q).

{

intro.

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

assert (Out B C G) by (conclude lemma_ray4).

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

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

assert (Cong A G A G) by (conclude cn_congruencereflexive).

assert (Cong B G B G) by (conclude cn_congruencereflexive).

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (CongA A B G A B C) by (conclude_def CongA ).

assert (CongA A B C A B G) by (conclude lemma_equalanglessymmetric).

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

contradict.

}

assert (¬ Col B C G).

{

intro.

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

assert (Out A G Q) by (conclude_def Out ).

assert (Col A G Q) by (conclude lemma_rayimpliescollinear).

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

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

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

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

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

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

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

assert (Col G Q B) by (conclude lemma_collinear5).

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

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

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

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

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

contradict.

}

assert (¬ BetS A Q G).

{

intro.

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

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

contradict.

}

assert (Out B C Q) by (conclude lemma_ray4).

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

assert (¬ BetS A G Q).

{

intro.

assert (CongA A B G A B G) by (conclude lemma_equalanglesreflexive).

assert (LtA A B G A B C) by (conclude_def LtA ).

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

assert (LtA D E F A B C) by (conclude lemma_angleorderrespectscongruence2).

contradict.

}

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

assert (eq G Q) by (conclude lemma_outerconnectivity).

assert (¬ ¬ LtA A B C D E F).

{

intro.

contradict.

}

close.

}

{

assert (¬ ¬ LtA A B C D E F).

{

intro.

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

assert (¬ Col P G B).

{

intro.

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

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

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

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

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

contradict.

}

let Tf:=fresh in

assert (Tf:∃ Q, (BetS B Q G ∧ BetS P R Q)) by (conclude postulate_Pasch_outer);destruct Tf as [Q];spliter.

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

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

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

assert (Out B G Q) by (conclude lemma_ray4).

assert (Out B Q G) by (conclude lemma_ray4).

assert (¬ BetS R C Q).

{

intro.

assert (Out B A R) by (conclude lemma_ray4).

assert (Out B G Q) by (conclude lemma_ray4).

assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).

assert (LtA A B C A B G) by (conclude_def LtA ).

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

assert (LtA A B C D E F) by (conclude lemma_angleorderrespectscongruence).

contradict.

}

assert (¬ BetS R Q C).

{

intro.

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

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

assert (Out B Q G) by (conclude lemma_ray4).

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

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

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (Cong B G B G) by (conclude cn_congruencereflexive).

assert (Cong A G A G) by (conclude cn_congruencereflexive).

assert (CongA A B G A B Q) by (conclude_def CongA ).

assert (Out B A R) by (conclude lemma_ray4).

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

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

assert (LtA A B G A B C) by (conclude_def LtA ).

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

assert (LtA D E F A B C) by (conclude lemma_angleorderrespectscongruence2).

contradict.

}

assert (eq Q C) by (conclude lemma_outerconnectivity).

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

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

assert (Out B C G) by (conclude cn_equalitysub).

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

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

assert (Out B Q G) by (conclude lemma_ray4).

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

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

assert (Cong B A B A) by (conclude cn_congruencereflexive).

assert (Cong B G B G) by (conclude cn_congruencereflexive).

assert (Cong A G A G) by (conclude cn_congruencereflexive).

assert (CongA A B G A B Q) by (conclude_def CongA ).

assert (CongA A B C A B G) by (conclude_def CongA ).

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

contradict.

}

close.

}

close.

}

close.

Qed.

End Euclid.