Require Export GeoCoq.Elements.OriginalProofs.proposition_47B.
Require Export GeoCoq.Elements.OriginalProofs.lemma_squareflip.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_47 : 
   forall A B C D E F G H K, 
   Triangle A B C -> Per B A C -> SQ A B F G -> TS G B A C -> SQ A C K H -> TS H C A B -> SQ B C E D -> TS D C B A ->
   exists X Y, PG B X Y D /\ BetS B X C /\ PG X C E Y /\ BetS D Y E /\ EF A B F G B X Y D /\ EF A C K H X C E Y.
Proof.
(* Goal: forall (A B C D E F G H K : @Point Ax0) (_ : @Triangle Ax0 A B C) (_ : @Per Ax0 B A C) (_ : @SQ Ax0 A B F G) (_ : @TS Ax0 G B A C) (_ : @SQ Ax0 A C K H) (_ : @TS Ax0 H C A B) (_ : @SQ Ax0 B C E D) (_ : @TS Ax0 D C B A), @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
intros.
let Tf:=fresh in
assert (Tf:exists M L, (PG B M L D /\ BetS B M C /\ PG M C E L /\ BetS D L E /\ BetS L M A /\ Per D L A /\ EF A B F G B M L D)) by (conclude proposition_47B);destruct Tf as [M[L]];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (nCol A B C) by (conclude_def Triangle ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (nCol A C B) by (forward_using lemma_NCorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Triangle A C B) by (conclude_def Triangle ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Per C A B) by (conclude lemma_8_2).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (SQ C B D E) by (conclude lemma_squareflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (TS D B C A) by (conclude lemma_oppositesideflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (PG B C E D) by (conclude lemma_squareparallelogram).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Par B C E D) by (conclude_def PG ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (TP B C E D) by (conclude lemma_paralleldef2B).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (OS E D B C) by (conclude_def TP ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (TS E B C A) by (conclude lemma_planeseparation).
let Tf:=fresh in
assert (Tf:exists m l, (PG C m l E /\ BetS C m B /\ PG m B D l /\ BetS E l D /\ BetS l m A /\ Per E l A /\ EF A C K H C m l E)) by (conclude proposition_47B);destruct Tf as [m[l]];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (neq E D) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (neq D E) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col E l D) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col D L E) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col D E L) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col D E l) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col E l L) by (conclude lemma_collinear4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (neq L E) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (neq E L) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Per E L A) by (conclude lemma_collinearright).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (eq l L) by (conclude lemma_droppedperpendicularunique).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (eq L l) by (conclude lemma_equalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (BetS L m A) by (conclude cn_equalitysub).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (BetS C M B) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col L m A) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col L M A) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col L A m) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col L A M) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (neq L A) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col A m M) by (conclude lemma_collinear4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col M m A) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col B M C) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col C B M) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col C m B) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col C B m) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (neq C B) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col B M m) by (conclude lemma_collinear4).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (Col M m B) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (~ neq M m).
(* Goal: not (@neq Ax0 M m) *)
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
 {
(* Goal: not (@neq Ax0 M m) *)
 intro.
(* Goal: False *)
 assert (Col m M A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col m M B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq m M) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col M A B) by (conclude lemma_collinear4).
(* Goal: False *)
 assert (Col M B A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col M B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq M B) by (forward_using lemma_betweennotequal).
(* 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.
 }
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (EF A C K H C M l E) by (conclude cn_equalitysub).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (EF A C K H C M L E) by (conclude cn_equalitysub).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
assert (EF A C K H M C E L) by (forward_using axiom_EFpermutation).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => and (@PG Ax0 B X Y D) (and (@BetS Ax0 B X C) (and (@PG Ax0 X C E Y) (and (@BetS Ax0 D Y E) (and (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D) (@EF Ax0 Ax1 Ax2 Ax A C K H X C E Y))))))) *)
close.
Qed.

End Euclid.


