Require Export GeoCoq.Elements.OriginalProofs.lemma_diagonalsbisect.

Section Euclid.

Context `{Ax:euclidean_euclidean}.

Lemma lemma_trapezoiddiagonals : 
   forall A B C D E, 
   PG A B C D -> BetS A E D ->
   exists X, BetS B X D /\ BetS C X E.
Proof.
(* Goal: forall (A B C D E : @Point Ax0) (_ : @PG Ax0 A B C D) (_ : @BetS Ax0 A E D), @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
intros.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (Par A B C D) by (conclude_def PG ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (Par A D B C) by (conclude_def PG ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (~ Meet A B C D) by (conclude_def Par ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (neq A B) by (conclude_def Par ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (neq C D) by (conclude_def Par ).
let Tf:=fresh in
assert (Tf:exists M, (Midpoint A M C /\ Midpoint B M D)) by (conclude lemma_diagonalsbisect);destruct Tf as [M];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (BetS A M C) by (conclude_def Midpoint ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (Cong A M M C) by (conclude_def Midpoint ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (BetS B M D) by (conclude_def Midpoint ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (Cong B M M D) by (conclude_def Midpoint ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (Cong B M D M) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (~ Col B D C).
(* Goal: not (@Col Ax0 B P C) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
 {
(* Goal: not (@Col Ax0 B P C) *)
 intro.
(* Goal: False *)
 assert (Col C D B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col A B B) by (conclude_def Col ).
(* Goal: False *)
 assert (Meet A B C D) by (conclude_def Meet ).
(* Goal: False *)
 contradict.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (Cong M A M C) by (forward_using lemma_congruenceflip).
let Tf:=fresh in
assert (Tf:exists P, (BetS B E P /\ BetS C D P)) by (conclude postulate_Euclid5);destruct Tf as [P];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
assert (~ Col B P C).
(* Goal: not (@Col Ax0 B P C) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
 {
(* Goal: not (@Col Ax0 B P C) *)
 intro.
(* Goal: False *)
 assert (Col P C B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col C D P) by (conclude_def Col ).
(* Goal: False *)
 assert (Col P C D) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq C P) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq P C) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col C B D) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col C D B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col A B B) by (conclude_def Col ).
(* Goal: False *)
 assert (Meet A B C D) by (conclude_def Meet ).
(* Goal: False *)
 contradict.
 }
let Tf:=fresh in
assert (Tf:exists H', (BetS B H' D /\ BetS C H' E)) by (conclude postulate_Pasch_inner);destruct Tf as [H'];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => and (@BetS Ax0 B X D) (@BetS Ax0 C X E)) *)
close.
Qed.

End Euclid.

