Require Export GeoCoq.Elements.OriginalProofs.lemma_raystrict.
Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear4.
Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthancongruence.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_crossbar : 
   forall A B C E U V, 
   Triangle A B C -> BetS A E C -> Out B A U -> Out B C V ->
   exists X, Out B E X /\ BetS U X V.
Proof.
(* Goal: forall (A B C E U V : @Point Ax0) (_ : @Triangle Ax0 A B C) (_ : @BetS Ax0 A E C) (_ : @Out Ax0 B A U) (_ : @Out Ax0 B C V), @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
intros.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (~ eq B E).
(* Goal: not (@eq Ax0 E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
 {
(* Goal: not (@eq Ax0 E B) *)
 intro.
(* Goal: False *)
 assert (~ BetS A B C).
(* Goal: not (@eq Ax0 E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
  {
(* Goal: not (@eq Ax0 E B) *)
  intro.
(* Goal: False *)
  assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (BetS A B C) by (conclude cn_equalitysub).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (~ eq B A).
(* Goal: not (@eq Ax0 E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
 {
(* Goal: not (@eq Ax0 E B) *)
 intro.
(* Goal: False *)
 assert (eq A B) by (conclude lemma_equalitysymmetric).
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (~ eq B C).
(* Goal: not (@eq Ax0 E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
 {
(* Goal: not (@eq Ax0 E B) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (neq B U) by (conclude lemma_raystrict).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (neq B V) by (conclude lemma_raystrict).
let Tf:=fresh in
assert (Tf:exists P, (BetS B A P /\ Cong A P B U)) by (conclude lemma_extension);destruct Tf as [P];spliter.
let Tf:=fresh in
assert (Tf:exists Q, (BetS B C Q /\ Cong C Q B V)) by (conclude lemma_extension);destruct Tf as [Q];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (~ Col B Q A).
(* Goal: not (@eq Ax0 E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
 {
(* Goal: not (@eq Ax0 E B) *)
 intro.
(* Goal: False *)
 assert (Col Q B A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col B C Q) by (conclude_def Col ).
(* Goal: False *)
 assert (Col Q B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq B Q) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq Q B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col B A C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists F, (BetS A F Q /\ BetS B E F)) by (conclude postulate_Pasch_outer);destruct Tf as [F];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS Q F A) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (~ Col B P Q).
(* Goal: not (@eq Ax0 E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
 {
(* Goal: not (@eq Ax0 E B) *)
 intro.
(* Goal: False *)
 assert (Col P B Q) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col B A P) by (conclude_def Col ).
(* Goal: False *)
 assert (Col P B A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq B P) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq P B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col B Q A) by (conclude lemma_collinear4).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists W, (BetS Q W P /\ BetS B F W)) by (conclude postulate_Pasch_outer);destruct Tf as [W];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS B E W) by (conclude lemma_3_6b).
let Tf:=fresh in
assert (Tf:exists J, (BetS J B U /\ BetS J B A)) by (conclude_def Out );destruct Tf as [J];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Cong A P P A) by (conclude cn_equalityreverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Cong B U A P) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Cong B U P A) by (conclude lemma_congruencetransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Cong P A B U) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS P A B) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Lt B U P B) by (conclude_def Lt ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Cong P B B P) by (conclude cn_equalityreverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Lt B U B P) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:exists S, (BetS B S P /\ Cong B S B U)) by (conclude_def Lt );destruct Tf as [S];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS J B P) by (conclude lemma_3_7b).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS J B S) by (conclude axiom_innertransitivity).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (eq S U) by (conclude lemma_extensionunique).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS B U P) by (conclude cn_equalitysub).
let Tf:=fresh in
assert (Tf:exists K, (BetS K B V /\ BetS K B C)) by (conclude_def Out );destruct Tf as [K];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Cong B V C Q) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Cong C Q Q C) by (conclude cn_equalityreverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Cong B V Q C) by (conclude lemma_congruencetransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Cong Q C B V) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS Q C B) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Lt B V Q B) by (conclude_def Lt ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Cong Q B B Q) by (conclude cn_equalityreverse).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Lt B V B Q) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:exists R, (BetS B R Q /\ Cong B R B V)) by (conclude_def Lt );destruct Tf as [R];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS K B Q) by (conclude lemma_3_7b).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS K B R) by (conclude axiom_innertransitivity).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (eq R V) by (conclude lemma_extensionunique).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS B V Q) by (conclude cn_equalitysub).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (~ Col Q P B).
(* Goal: not (@eq Ax0 E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
 {
(* Goal: not (@eq Ax0 E B) *)
 intro.
(* Goal: False *)
 assert (Col B P Q) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists M, (BetS Q M U /\ BetS B M W)) by (conclude postulate_Pasch_inner);destruct Tf as [M];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS U M Q) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (~ Col U Q B).
(* Goal: not (@eq Ax0 E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
 {
(* Goal: not (@eq Ax0 E B) *)
 intro.
(* Goal: False *)
 assert (Col B U P) by (conclude_def Col ).
(* Goal: False *)
 assert (Col B U Q) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq B U) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col U B P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col U B Q) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq U B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col B P Q) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col Q P B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
rename_H H;let Tf:=fresh in
assert (Tf:exists H, (BetS U H V /\ BetS B H M)) by (conclude postulate_Pasch_inner);destruct Tf as [H];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (~ eq E B).
(* Goal: not (@eq Ax0 E B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
 {
(* Goal: not (@eq Ax0 E B) *)
 intro.
(* Goal: False *)
 assert (eq B E) by (conclude lemma_equalitysymmetric).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists N, (BetS E B N /\ Cong B N B E)) by (conclude lemma_extension);destruct Tf as [N];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS N B E) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS B H W) by (conclude lemma_3_6b).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS N B W) by (conclude lemma_3_7b).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (BetS N B H) by (conclude axiom_innertransitivity).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
assert (Out B E H) by (conclude_def Out ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@Out Ax0 B E X) (@BetS Ax0 U X V)) *)
close.
Qed.

End Euclid.


