Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear4.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_Pasch_outer2 : 
   forall A B C P Q, 
   BetS A P C -> BetS B C Q -> nCol B P A ->
   exists X, BetS A X Q /\ BetS B P X.
Proof.
(* Goal: forall (A B C P Q : @Point Ax) (_ : @BetS Ax A P C) (_ : @BetS Ax B C Q) (_ : @nCol Ax B P A), @ex (@Point Ax) (fun X : @Point Ax => and (@BetS Ax A X Q) (@BetS Ax B P X)) *)
intros.
(* Goal: @ex (@Point Ax) (fun X : @Point Ax => and (@BetS Ax A X Q) (@BetS Ax B P X)) *)
assert (~ Col B Q A).
(* Goal: not (@eq Ax Q A) *)
(* Goal: False *)
 {
(* Goal: not (@eq Ax Q A) *)
 intro.
(* Goal: False *)
 assert (Col A P C) by (conclude_def Col ).
(* Goal: False *)
 assert (Col B C Q) by (conclude_def Col ).
(* Goal: False *)
 assert (Col B Q C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (~ eq Q A).
(* Goal: not (@eq Ax Q A) *)
(* Goal: False *)
  {
(* Goal: not (@eq Ax Q A) *)
  intro.
(* Goal: False *)
  assert (Col B A C) by (conclude cn_equalitysub).
(* Goal: False *)
  assert (Col C A B) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (Col C A P) by (forward_using lemma_collinearorder).
(* Goal: False *)
  assert (neq A C) by (forward_using lemma_betweennotequal).
(* Goal: False *)
  assert (neq C A) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
  assert (Col A B P) by (conclude lemma_collinear4).
(* Goal: False *)
  assert (Col B P A) by (forward_using lemma_collinearorder).
(* Goal: False *)
  contradict.
  }
(* Goal: False *)
 assert (Col B Q C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq B Q) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col Q A C) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A C Q) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col A C P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq A C) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col C Q P) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col C Q B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq C Q) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (Col Q P B) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col Q B P) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col Q B A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq Q B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col B P A) by (conclude lemma_collinear4).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists E, (BetS A E Q /\ BetS B P E)) by (conclude postulate_Pasch_outer);destruct Tf as [E];spliter.
(* Goal: @ex (@Point Ax) (fun X : @Point Ax => and (@BetS Ax A X Q) (@BetS Ax B P X)) *)
close.
Qed.

End Euclid.


