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.