# Library GeoCoq.Elements.OriginalProofs.lemma_Pasch_outer2

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear4.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_Pasch_outer2 :

∀ A B C P Q,

BetS A P C → BetS B C Q → nCol B P A →

∃ X, BetS A X Q ∧ BetS B P X.

Proof.

intros.

assert (¬ Col B Q A).

{

intro.

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

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

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

assert (¬ eq Q A).

{

intro.

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

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

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

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

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

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

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

contradict.

}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

contradict.

}

let Tf:=fresh in

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

close.

Qed.

End Euclid.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_Pasch_outer2 :

∀ A B C P Q,

BetS A P C → BetS B C Q → nCol B P A →

∃ X, BetS A X Q ∧ BetS B P X.

Proof.

intros.

assert (¬ Col B Q A).

{

intro.

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

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

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

assert (¬ eq Q A).

{

intro.

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

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

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

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

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

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

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

contradict.

}

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

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

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

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

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

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

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

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

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

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

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

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

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

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

contradict.

}

let Tf:=fresh in

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

close.

Qed.

End Euclid.