Require Export GeoCoq.Elements.OriginalProofs.lemma_crossbar.
Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglesreflexive.
Require Export GeoCoq.Elements.OriginalProofs.lemma_sameside2.
Require Export GeoCoq.Elements.OriginalProofs.proposition_07.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_crossbar2 : 
   forall A G H P S T, 
   LtA H G A H G P -> OS A P G H -> Out G H S -> Out G P T ->
   exists X, BetS T X S /\ Out G A X.
Proof.
(* Goal: forall (A G H P S T : @Point Ax0) (_ : @LtA Ax0 H G A H G P) (_ : @OS Ax0 A P G H) (_ : @Out Ax0 G H S) (_ : @Out Ax0 G P T), @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
intros.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (nCol G H P) by (conclude_def OS ).
let Tf:=fresh in
assert (Tf:exists J K L, (BetS L K J /\ Out G H L /\ Out G P J /\ CongA H G A H G K)) by (conclude_def LtA );destruct Tf as [J[K[L]]];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (nCol H G K) by (conclude lemma_equalanglesNC).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (~ Col L G J).
(* Goal: not (@Col Ax0 H G M) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
 {
(* Goal: not (@Col Ax0 H G M) *)
 intro.
(* Goal: False *)
 assert (Col G H L) by (conclude lemma_rayimpliescollinear).
(* Goal: False *)
 assert (Col G P J) by (conclude lemma_rayimpliescollinear).
(* Goal: False *)
 assert (Col L G H) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq G L) by (conclude lemma_raystrict).
(* Goal: False *)
 assert (neq L G) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col G J H) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col J G H) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col J G P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq G J) by (conclude lemma_raystrict).
(* Goal: False *)
 assert (neq J G) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col G H P) by (conclude lemma_collinear4).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Triangle L G J) by (conclude_def Triangle ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Out G J T) by (conclude lemma_ray3).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Out G L S) by (conclude lemma_ray3).
let Tf:=fresh in
assert (Tf:exists M, (Out G K M /\ BetS S M T)) by (conclude lemma_crossbar);destruct Tf as [M];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (BetS T M S) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (CongA H G K H G A) by (conclude lemma_equalanglessymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (neq G A) by (forward_using lemma_angledistinct).
(* Goal: False *)
assert (neq G M) by (conclude lemma_raystrict).
let Tf:=fresh in
assert (Tf:exists N, (Out G A N /\ Cong G N G M)) by (conclude lemma_layoff);destruct Tf as [N];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (eq H H) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (~ eq G H).
(* Goal: not (@Col Ax0 H G M) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
 {
(* Goal: not (@Col Ax0 H G M) *)
 intro.
(* Goal: False *)
 assert (Col G H P) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Out G H H) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (~ Col H G M).
(* Goal: not (@Col Ax0 H G M) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
 {
(* Goal: not (@Col Ax0 H G M) *)
 intro.
(* Goal: False *)
 assert (Col G K M) by (conclude lemma_rayimpliescollinear).
(* Goal: False *)
 assert (Col M G K) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col M G H) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq G M) by (conclude lemma_raystrict).
(* Goal: False *)
 assert (neq M G) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col G K H) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col H G K) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (CongA H G M H G M) by (conclude lemma_equalanglesreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Out G M K) by (conclude lemma_ray5).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (CongA H G M H G K) by (conclude lemma_equalangleshelper).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (CongA H G M H G A) by (conclude lemma_equalanglestransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (nCol H G A) by (conclude lemma_equalanglesNC).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (CongA H G A H G A) by (conclude lemma_equalanglesreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (CongA H G A H G N) by (conclude lemma_equalangleshelper).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (CongA H G M H G N) by (conclude lemma_equalanglestransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (CongA H G N H G M) by (conclude lemma_equalanglessymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Cong G H G H) by (conclude cn_congruencereflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Cong H N H M) by (conclude proposition_04).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (eq G G) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Col G G H) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (OS A T G H) by (conclude lemma_sameside2).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (neq S M) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Out S M T) by (conclude lemma_ray4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Out S T M) by (conclude lemma_ray5).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Col G H S) by (conclude lemma_rayimpliescollinear).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Col G S H) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (OS A M G H) by (conclude lemma_sameside2).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (OS M A G H) by (forward_using lemma_samesidesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (OS M N G H) by (conclude lemma_sameside2).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Cong N H M H) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Cong M H N H) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Cong N G M G) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Cong M G N G) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (eq M N) by (conclude proposition_07).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (eq N M) by (conclude lemma_equalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
assert (Out G A M) by (conclude cn_equalitysub).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 T X S) (@Out Ax0 G A X)) *)
close.
Qed.

End Euclid.


