Require Export GeoCoq.Elements.OriginalProofs.proposition_47A.
Require Export GeoCoq.Elements.OriginalProofs.lemma_angleaddition.
Require Export GeoCoq.Elements.OriginalProofs.proposition_41.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_47B : 
   forall A B C D E F G, 
   Triangle A B C -> Per B A C -> SQ A B F G -> TS G B A C -> 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 /\ BetS Y X A /\ Per D Y A /\ EF A B F G B X Y D.
Proof.
(* Goal: forall (A B C D E F G : @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 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
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)) by (conclude proposition_47A);destruct Tf as [M[L]];spliter.

let Tf:=fresh in
assert (Tf:exists N, (BetS D N A /\ Col C B N /\ nCol C B D)) by (conclude_def TS );destruct Tf as [N];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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Per G A B) by (conclude_def SQ ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (BetS G A C) by (conclude lemma_righttogether).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Per A B F) by (conclude_def SQ ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Per F B A) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Per D B C) by (conclude_def SQ ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (PG A B F G) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par A B F G) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par A B G F) by (forward_using lemma_parallelflip).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (TP A B G F) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (OS G F A B) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (OS F G A B) by (forward_using lemma_samesidesymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (TS G A B C) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (TS F A B C) by (conclude lemma_planeseparation).
let Tf:=fresh in
assert (Tf:exists a, (BetS F a C /\ Col A B a /\ nCol A B F)) by (conclude_def TS );destruct Tf as [a];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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col B A 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par A G B F) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par A G F B) by (forward_using lemma_parallelflip).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col G A 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col A G C) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq G C) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq C G) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par F B A G) by (conclude lemma_parallelsymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par F B C G) by (conclude lemma_collinearparallel).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par F B G C) by (forward_using lemma_parallelflip).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (~ Meet F B G C) by (conclude_def Par ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq A C) by (forward_using lemma_NCdistinct).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol A B F) by (forward_using lemma_parallelNC).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq F A) by (forward_using lemma_NCdistinct).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq F B) by (forward_using lemma_NCdistinct).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col F B 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (BetS B a A) by (conclude lemma_collinearbetween).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq B 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Out B a A) by (conclude lemma_ray4).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq B F) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (eq F F) by (conclude cn_equalityreflexive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Out B F F) by (conclude lemma_ray4).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol A B F) by (forward_using lemma_parallelNC).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol F B A) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA F B A F B A) by (conclude lemma_equalanglesreflexive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Out B A a) by (conclude lemma_ray5).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA F B A F B a) by (conclude lemma_equalangleshelper).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq B C) by (forward_using lemma_NCdistinct).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (eq C C) by (conclude cn_equalityreflexive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Out B C C) by (conclude lemma_ray4).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA A B C A B C) by (conclude lemma_equalanglesreflexive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA A B C a B C) by (conclude lemma_equalangleshelper).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (SumA F B A A B C F B C) by (conclude_def SumA ).
let Tf:=fresh in
assert (Tf:exists c, (BetS D c A /\ Col C B c /\ nCol C B D)) by (conclude_def TS );destruct Tf as [c];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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par B D C E) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par C E B D) by (conclude lemma_parallelsymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par C E D B) by (forward_using lemma_parallelflip).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col B C c) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col C B c) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq C B) by (forward_using lemma_NCdistinct).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col B M c) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par B D M L) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col M L 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq A 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par B D A L) by (conclude lemma_collinearparallel).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par D B L A) by (forward_using lemma_parallelflip).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (~ Meet D B L A) by (conclude_def Par ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol B D L) by (forward_using lemma_parallelNC).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq D B) by (forward_using lemma_NCdistinct).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq M 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq L M) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (eq D D) by (conclude cn_equalityreflexive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col D B 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (BetS B c M) by (conclude lemma_collinearbetween).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (BetS B c C) by (conclude lemma_3_6b).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol D B A) by (forward_using lemma_parallelNC).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (~ eq B c).
(* Goal: not (@Col Ax0 C B F) *)
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
 {
(* Goal: not (@Col Ax0 C B F) *)
 intro.
(* Goal: False *)
 assert (Col D B c) by (conclude_def Col ).
(* Goal: False *)
 assert (Col D c A) by (conclude_def Col ).
(* Goal: False *)
 assert (Col c D B) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Col c D A) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (neq D c) by (forward_using lemma_betweennotequal).
(* Goal: False *)
 assert (neq c D) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (Col D B A) by (conclude lemma_collinear4).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Out B c C) by (conclude lemma_ray4).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Out B C c) by (conclude lemma_ray5).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol C B A) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA C B A C B A) by (conclude lemma_equalanglesreflexive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq B A) by (forward_using lemma_NCdistinct).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Out B A A) by (conclude lemma_ray4).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA C B A c B A) by (conclude lemma_equalangleshelper).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol C D B) by (forward_using lemma_parallelNC).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol D B C) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA D B C D B C) by (conclude lemma_equalanglesreflexive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (neq B D) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Out B D D) by (conclude lemma_ray4).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA D B C D B c) by (conclude lemma_equalangleshelper).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (SumA D B C C B A D B A) by (conclude_def SumA ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA F B A D B C) by (conclude lemma_Euclid4).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA A B C C B A) by (conclude lemma_ABCequalsCBA).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA F B C D B A) by (conclude lemma_angleaddition).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA D B A F B C) by (conclude lemma_equalanglessymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (~ Col C B F).
(* Goal: not (@Col Ax0 C B F) *)
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
 {
(* Goal: not (@Col Ax0 C B F) *)
 intro.
(* Goal: False *)
 assert (Col F B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 assert (Per C B A) by (conclude lemma_collinearright).
(* Goal: False *)
 assert (~ Per C B A) by (conclude lemma_8_7).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol F B C) by (assert (nCol C B F) by auto;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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA F B C C B F) by (conclude lemma_ABCequalsCBA).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA D B A C B F) by (conclude lemma_equalanglestransitive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Cong A B B F) by (conclude_def SQ ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Cong A B F B) by (forward_using lemma_congruenceflip).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Cong F B A B) by (conclude lemma_congruencesymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Cong B F B A) by (forward_using lemma_congruenceflip).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Cong B A B F) by (conclude lemma_congruencesymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Cong B C D B) by (conclude_def SQ ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Cong D B B C) by (conclude lemma_congruencesymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Cong B D B C) by (forward_using lemma_congruenceflip).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert ((Cong D A C F /\ CongA B D A B C F /\ CongA B A D B F C)) by (conclude proposition_04).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Cong A D F C) by (forward_using lemma_congruenceflip).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (CongA B F C B A D) by (conclude lemma_equalanglessymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol B A D) by (conclude lemma_equalanglesNC).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol A B D) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Triangle A B D) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Cong_3 A B D F B C) by (conclude_def Cong_3 ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET A B D F B C) by (conclude axiom_congruentequal).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par B M L 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par B D M L) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par M L B D) by (conclude lemma_parallelsymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Par M B D L) by (forward_using lemma_parallelflip).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (PG M B D L) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col M L 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET M B D A B D) by (conclude proposition_41).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (PG A B F G) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (PG B A G F) by (conclude lemma_PGflip).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col G A 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col A G C) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET A B F C B F) by (conclude proposition_41).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET A B F F B C) by (forward_using axiom_ETpermutation).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET F B C A B D) by (conclude axiom_ETsymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET A B F A B D) by (conclude axiom_ETtransitive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET A B D M B D) by (conclude axiom_ETsymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET A B F M B D) by (conclude axiom_ETtransitive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Cong_3 A B F F G A) by (conclude proposition_34).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET A B F F G A) by (conclude axiom_congruentequal).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (PG B M L D) by (conclude lemma_PGflip).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Cong_3 M B D D L M) by (conclude proposition_34).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET M B D D L M) by (conclude axiom_congruentequal).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET F G A A B F) by (conclude axiom_ETsymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET F G A A B D) by (conclude axiom_ETtransitive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET F G A M B D) by (conclude axiom_ETtransitive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET F G A D L M) by (conclude axiom_ETtransitive).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET F G A D M L) by (forward_using axiom_ETpermutation).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET D M L F G A) by (conclude axiom_ETsymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET D M L F A G) by (forward_using axiom_ETpermutation).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET F A G D M L) by (conclude axiom_ETsymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET A B F D M B) by (forward_using axiom_ETpermutation).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET D M B A B F) by (conclude axiom_ETsymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET D M B F A B) by (forward_using axiom_ETpermutation).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (ET F A B D M B) by (conclude axiom_ETsymmetric).
let Tf:=fresh in
assert (Tf:exists m, (Midpoint A m F /\ Midpoint B m G)) by (conclude lemma_diagonalsbisect);destruct Tf as [m];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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (BetS A m F) by (conclude_def Midpoint ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (BetS B m G) by (conclude_def Midpoint ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (BetS F m A) by (conclude axiom_betweennesssymmetry).
let Tf:=fresh in
assert (Tf:exists n, (Midpoint B n L /\ Midpoint M n D)) by (conclude lemma_diagonalsbisect);destruct Tf as [n];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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (BetS B n L) by (conclude_def Midpoint ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (BetS M n D) by (conclude_def Midpoint ).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (BetS D n M) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col M n 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (Col D M n) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol B M D) by (forward_using lemma_parallelNC).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (nCol D M 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (EF F B A G D B M L) by (conclude axiom_paste3).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (EF F B A G B M L D) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (EF B M L D F B A G) by (conclude axiom_EFsymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (EF B M L D A B F G) 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
assert (EF A B F G B M L D) by (conclude axiom_EFsymmetric).
(* 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 (@BetS Ax0 Y X A) (and (@Per Ax0 D Y A) (@EF Ax0 Ax1 Ax2 Ax A B F G B X Y D)))))))) *)
close.
Qed.

End Euclid.


