Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelsymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_paralleldef2B.
Require Export GeoCoq.Elements.OriginalProofs.lemma_parallelNC.
Require Export GeoCoq.Elements.OriginalProofs.lemma_planeseparation.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_parallelPasch : 
   forall A B C D E, 
   PG A B C D -> BetS A D E ->
   exists X, BetS B X E /\ BetS C X D.
Proof.
(* Goal: forall (A B C D E : @Point Ax0) (_ : @PG Ax0 A B C D) (_ : @BetS Ax0 A D E), @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
intros.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (Par A B C D) by (conclude_def PG ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (Par A D B C) by (conclude_def PG ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (Par C D A B) by (conclude lemma_parallelsymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (TP C D A B) by (conclude lemma_paralleldef2B).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (OS A B C D) by (conclude_def TP ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (OS B A C D) by (forward_using lemma_samesidesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (neq A D) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (Col A D D) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (Col A D E) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (Col D D E) by (conclude lemma_collinear4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (Col E D D) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (Col C D D) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (nCol A C D) by (forward_using lemma_parallelNC).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (nCol C D A) by (forward_using lemma_NCorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (TS A C D E) by (conclude_def TS ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (TS B C D E) by (conclude lemma_planeseparation).
rename_H H;let Tf:=fresh in
assert (Tf:exists H, (BetS B H E /\ Col C D H /\ nCol C D B)) by (conclude_def TS );destruct Tf as [H];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (BetS E H B) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (Col D C H) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (neq A D) by (conclude_def Par ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (~ Meet A D B C) by (conclude_def Par ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (~ Meet E D C B).
(* Goal: not (@Meet Ax0 E D C B) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
 {
(* Goal: not (@Meet Ax0 E D C B) *)
 intro.
 let Tf:=fresh in
 assert (Tf:exists p, (neq E D /\ neq C B /\ Col E D p /\ Col C B p)) by (conclude_def Meet );destruct Tf as [p];spliter.
(* Goal: False *)
 assert (neq B C) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col B C p) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col E D A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col D A p) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col A D p) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Meet A D B C) by (conclude_def Meet ).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (neq D E) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (neq E D) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (neq B C) by (conclude_def Par ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (Col C C B) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (BetS D H C) by (conclude lemma_collinearbetween).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
assert (BetS C H D) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X E) (@BetS Ax0 C X D)) *)
close.
Qed.

End Euclid.


