Library GeoCoq.Elements.OriginalProofs.proposition_23C

Require Export GeoCoq.Elements.OriginalProofs.proposition_23B.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_23C :
   ∀ A B C D E P,
   neq A B → nCol D C E → nCol A B P →
   ∃ X Y, Out A B Y ∧ CongA X A Y D C E ∧ OS X P A B.
Proof.
intros.
assert (neq B A) by (conclude lemma_inequalitysymmetric).
assert (¬ eq P A).
 {
 intro.
 assert (eq A P) by (conclude lemma_equalitysymmetric).
 assert (Col A B P) by (conclude_def Col ).
 contradict.
 }
let Tf:=fresh in
assert (Tf:∃ Q, (BetS P A Q ∧ Cong A Q P A)) by (conclude postulate_extension);destruct Tf as [Q];spliter.
assert (eq A A) by (conclude cn_equalityreflexive).
assert (Col A B A) by (conclude_def Col ).
assert (TS P A B Q) by (conclude_def TS ).
assert (¬ Col A B Q).
 {
 intro.
 assert (Col P A Q) by (conclude_def Col ).
 assert (Col Q A B) by (forward_using lemma_collinearorder).
 assert (Col Q A P) by (forward_using lemma_collinearorder).
 assert (neq A Q) by (forward_using lemma_betweennotequal).
 assert (neq Q A) by (conclude lemma_inequalitysymmetric).
 assert (Col A B P) by (conclude lemma_collinear4).
 contradict.
 }
let Tf:=fresh in
assert (Tf:∃ F G, (Out A B G ∧ CongA F A G D C E ∧ TS F A B Q)) by (conclude proposition_23B);destruct Tf as [F[G]];spliter.
let Tf:=fresh in
assert (Tf:∃ J, (BetS F J Q ∧ Col A B J ∧ nCol A B F)) by (conclude_def TS );destruct Tf as [J];spliter.
assert (OS F P A B) by (conclude_def OS ).
close.
Qed.

End Euclid.