Require Export GeoCoq.Elements.OriginalProofs.proposition_42B.
Require Export GeoCoq.Elements.OriginalProofs.proposition_44A.

Section Euclid.

Context `{Ax:area}.

Lemma proposition_44 : 
   forall A B D J N R a b c, 
   Triangle a b c -> nCol J D N -> nCol A B R ->
   exists X Y Z, PG A B X Y /\ CongA A B X J D N /\ EF a b Z c A B X Y /\ Midpoint b Z c /\ TS X A B R.
Proof.
(* Goal: forall (A B D J N R a b c : @Point Ax0) (_ : @Triangle Ax0 a b c) (_ : @nCol Ax0 J D N) (_ : @nCol Ax0 A B R), @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
intros.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (neq A B) by (forward_using lemma_NCdistinct).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (nCol a b c) by (conclude_def Triangle ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (neq b c) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:exists m, (BetS b m c /\ Cong m b m c)) by (conclude proposition_10);destruct Tf as [m];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Cong b m m c) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Midpoint b m c) by (conclude_def Midpoint ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (neq m c) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists E, (BetS A B E /\ Cong B E m c)) by (conclude lemma_extension);destruct Tf as [E];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (neq B E) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Col A B E) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Col B A E) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Col B A B) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (nCol B A R) by (forward_using lemma_NCorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (nCol B E R) by (conclude lemma_NChelper).
let Tf:=fresh in
assert (Tf:exists g e, (Out B E e /\ CongA g B e J D N /\ OS g R B E)) by (conclude proposition_23C);destruct Tf as [g[e]];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists P, (BetS B A P /\ Cong A P B A)) by (conclude lemma_extension);destruct Tf as [P];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (neq B E) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (neq E B) by (conclude lemma_inequalitysymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (neq b m) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists Q, (BetS E B Q /\ Cong B Q b m)) by (conclude lemma_extension);destruct Tf as [Q];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Cong b m m c) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Cong B Q m c) by (conclude lemma_congruencetransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Cong m c B E) by (conclude lemma_congruencesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Cong B Q B E) by (conclude lemma_congruencetransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (BetS Q B E) by (conclude axiom_betweennesssymmetry).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Cong Q B B E) by (forward_using lemma_congruenceflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Midpoint Q B E) by (conclude_def Midpoint ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (nCol B A R) by (forward_using lemma_NCorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Col A B E) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Col B A E) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (neq B E) by (forward_using lemma_betweennotequal).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (nCol B E R) by (conclude lemma_NChelper).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (nCol R B E) by (forward_using lemma_NCorder).
let Tf:=fresh in
assert (Tf:exists G F, (PG G B E F /\ EF a b m c G B E F /\ CongA E B G J D N /\ OS R G B E)) by (conclude proposition_42B);destruct Tf as [G[F]];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (PG B E F G) by (conclude lemma_PGrotate).
let Tf:=fresh in
assert (Tf:exists M L, (PG A B M L /\ CongA A B M J D N /\ EF B E F G L M B A /\ BetS G B M)) by (conclude proposition_44A);destruct Tf as [M[L]];spliter.
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Col A B B) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Par G B E F) by (conclude_def PG ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (nCol G B E) by (forward_using lemma_parallelNC).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (nCol E B G) by (forward_using lemma_NCorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Col E B A) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Col E B B) by (conclude_def Col ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (nCol A B G) by (conclude lemma_NChelper).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (TS G A B M) by (conclude_def TS ).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (EF a b m c B E F G) by (forward_using axiom_EFpermutation).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (EF a b m c L M B A) by (conclude axiom_EFtransitive).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (EF a b m c A B M L) by (forward_using axiom_EFpermutation).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (Col B E A) by (forward_using lemma_collinearorder).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (OS R G B A) by (conclude lemma_samesidecollinear).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (OS R G A B) by (conclude lemma_samesideflip).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (TS R A B M) by (conclude lemma_planeseparation).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
assert (TS M A B R) by (conclude lemma_oppositesidesymmetric).
(* Goal: @ex (@Point Ax0) (fun X : @Point Ax0 => @ex (@Point Ax0) (fun Y : @Point Ax0 => @ex (@Point Ax0) (fun Z : @Point Ax0 => and (@PG Ax0 A B X Y) (and (@CongA Ax0 A B X J D N) (and (@EF Ax0 Ax1 Ax2 Ax a b Z c A B X Y) (and (@Midpoint Ax0 b Z c) (@TS Ax0 X A B R))))))) *)
close.
Qed.

End Euclid.


