Require Export GeoCoq.Elements.OriginalProofs.proposition_23B.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_23C : 
   forall A B C D E P, 
   neq A B -> nCol D C E -> nCol A B P ->
   exists X Y, Out A B Y /\ CongA X A Y D C E /\ OS X P A B.
Proof.
(* Goal: forall (A B C D E P : @Point Ax0) (_ : @neq Ax0 A B) (_ : @nCol Ax0 D C E) (_ : @nCol Ax0 A B P), @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (and (@CongA Ax0 X A Y D C E) (@OS Ax0 X P A B)))) *)
intros.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (and (@CongA Ax0 X A Y D C E) (@OS Ax0 X P A B)))) *)
assert (~ eq P A).
(* Goal: not (@Col Ax0 A B Q) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (and (@CongA Ax0 X A Y D C E) (@OS Ax0 X P A B)))) *)
 {
(* Goal: not (@Col Ax0 A B Q) *)
 intro.
(* Goal: False *)
 assert (eq A P) by (conclude lemma_equalitysymmetric).
(* Goal: False *)
 assert (Col A B P) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists Q, (BetS P A Q /\ Cong A Q P A)) by (conclude lemma_extension);destruct Tf as [Q];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (and (@CongA Ax0 X A Y D C E) (@OS Ax0 X P A B)))) *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (and (@CongA Ax0 X A Y D C E) (@OS Ax0 X P A B)))) *)
assert (Col A B A) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (and (@CongA Ax0 X A Y D C E) (@OS Ax0 X P A B)))) *)
assert (~ Col A B Q).
(* Goal: not (@Col Ax0 A B Q) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (and (@CongA Ax0 X A Y D C E) (@OS Ax0 X P A B)))) *)
 {
(* Goal: not (@Col Ax0 A B Q) *)
 intro.
(* Goal: False *)
 assert (Col P A Q) by (conclude_def Col ).
(* Goal: False *)
 assert (Col Q A B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col Q A P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq A Q) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq Q A) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col A B P) by (conclude lemma_collinear4).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists 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:exists J, (BetS F J Q /\ Col A B J /\ nCol A B F)) by (conclude_def TS );destruct Tf as [J];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (and (@CongA Ax0 X A Y D C E) (@OS Ax0 X P A B)))) *)
assert (OS F P A B) by (conclude_def OS ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (and (@CongA Ax0 X A Y D C E) (@OS Ax0 X P A B)))) *)
close.
Qed.

End Euclid.


