# Library GeoCoq.Elements.OriginalProofs.lemma_9_5b

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear4.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_9_5b :

∀ A B C P Q R,

TS P A B C → BetS R Q P → nCol C P R → Col A B R →

TS Q A B C.

Proof.

intros.

let Tf:=fresh in

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

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

let Tf:=fresh in

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

assert (Col R S F) by (conclude_def Col ).

assert (¬ eq A B).

{

intro.

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

contradict.

}

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

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

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

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

assert (Col S F B) by (conclude lemma_collinear4).

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

assert (Col S B F) by (forward_using lemma_collinearorder).

assert (Col A B F).

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

{

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

assert (Col R S F) by (conclude_def Col ).

assert (Col R B F) by (conclude cn_equalitysub).

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

assert (¬ eq R B).

{

intro.

assert (eq R S) by (conclude cn_equalitysub).

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

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

contradict.

}

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

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

close.

}

{

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

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

close.

}

assert (¬ Col A B Q).

{

intro.

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

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

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

assert (Col R Q F).

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

{

assert (¬ eq A R).

{

intro.

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

contradict.

}

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

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

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

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

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

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

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

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

close.

}

{

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

close.

}

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

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

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

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

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

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

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

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

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

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

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

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

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

contradict.

}

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

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

close.

Qed.

End Euclid.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_9_5b :

∀ A B C P Q R,

TS P A B C → BetS R Q P → nCol C P R → Col A B R →

TS Q A B C.

Proof.

intros.

let Tf:=fresh in

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

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

let Tf:=fresh in

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

assert (Col R S F) by (conclude_def Col ).

assert (¬ eq A B).

{

intro.

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

contradict.

}

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

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

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

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

assert (Col S F B) by (conclude lemma_collinear4).

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

assert (Col S B F) by (forward_using lemma_collinearorder).

assert (Col A B F).

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

{

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

assert (Col R S F) by (conclude_def Col ).

assert (Col R B F) by (conclude cn_equalitysub).

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

assert (¬ eq R B).

{

intro.

assert (eq R S) by (conclude cn_equalitysub).

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

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

contradict.

}

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

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

close.

}

{

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

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

close.

}

assert (¬ Col A B Q).

{

intro.

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

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

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

assert (Col R Q F).

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

{

assert (¬ eq A R).

{

intro.

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

contradict.

}

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

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

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

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

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

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

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

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

close.

}

{

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

close.

}

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

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

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

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

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

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

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

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

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

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

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

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

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

contradict.

}

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

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

close.

Qed.

End Euclid.