Require Export GeoCoq.Elements.OriginalProofs.proposition_20.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TGsymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_TGflip.
Require Export GeoCoq.Elements.OriginalProofs.proposition_22.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_23 : 
   forall A B C D E, 
   neq A B -> nCol D C E ->
   exists X Y, Out A B Y /\ CongA X A Y D C E.
Proof.
(* Goal: forall (A B C D E : @Point Ax0) (_ : @neq Ax0 A B) (_ : @nCol Ax0 D C E), @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
intros.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (~ Col E C D).
(* Goal: not (@eq Ax0 A G) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
 {
(* Goal: not (@eq Ax0 A G) *)
 intro.
(* Goal: False *)
 assert (Col D C E) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (~ Col C E D).
(* Goal: not (@eq Ax0 A G) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
 {
(* Goal: not (@eq Ax0 A G) *)
 intro.
(* Goal: False *)
 assert (Col D C E) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (Triangle D C E) by (conclude_def Triangle ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (Triangle C E D) by (conclude_def Triangle ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (Triangle E C D) by (conclude_def Triangle ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (TG C D D E C E) by (conclude proposition_20).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (TG C E E D C D) by (conclude proposition_20).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (TG E C C D E D) by (conclude proposition_20).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (TG C D E C E D) by (conclude lemma_TGsymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (TG C D D E E C) by (forward_using lemma_TGflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (TG D E C D E C) by (conclude lemma_TGsymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (TG E D C D E C) by (forward_using lemma_TGflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (TG C D E D E C) by (conclude lemma_TGsymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (TG E C E D C D) by (forward_using lemma_TGflip).
let Tf:=fresh in
assert (Tf:exists G F, (Cong A G E C /\ Cong A F C D /\ Cong G F E D /\ Out A B G /\ Triangle A G F)) 
 by (conclude proposition_22);destruct Tf as [G[F]];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (Cong A G C E) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (Cong F G D E) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (eq E E) 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) (@CongA Ax0 X A Y D C E))) *)
assert (eq D D) 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) (@CongA Ax0 X A Y D C E))) *)
assert (eq F F) 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) (@CongA Ax0 X A Y D C E))) *)
assert (eq G G) 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) (@CongA Ax0 X A Y D C E))) *)
assert (~ eq C E).
(* Goal: not (@eq Ax0 A G) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
 {
(* Goal: not (@eq Ax0 A G) *)
 intro.
(* Goal: False *)
 assert (Col D C E) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (~ eq C D).
(* Goal: not (@eq Ax0 A G) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
 {
(* Goal: not (@eq Ax0 A G) *)
 intro.
(* Goal: False *)
 assert (Col C D E) by (conclude_def Col ).
(* Goal: False *)
 assert (Col D C E) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (Out C E E) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (Out C D D) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (~ Col F A G).
(* Goal: not (@eq Ax0 A G) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
 {
(* Goal: not (@eq Ax0 A G) *)
 intro.
(* Goal: False *)
 assert (Col A G F) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (nCol A G F) by (conclude_def Triangle ).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (~ eq A F).
(* Goal: not (@eq Ax0 A G) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
 {
(* Goal: not (@eq Ax0 A G) *)
 intro.
(* Goal: False *)
 assert (Col A F G) by (conclude_def Col ).
(* Goal: False *)
 assert (Col F A G) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (Out A F F) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (~ eq A G).
(* Goal: not (@eq Ax0 A G) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
 {
(* Goal: not (@eq Ax0 A G) *)
 intro.
(* Goal: False *)
 assert (Col A G F) by (conclude_def Col ).
(* Goal: False *)
 assert (Col F A G) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (Out A G G) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
assert (CongA F A G D C E) by (conclude_def CongA ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@Out Ax0 A B Y) (@CongA Ax0 X A Y D C E))) *)
close.
Qed.

End Euclid.


