Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NChelper.
Require Export GeoCoq.Elements.OriginalProofs.lemma_oppositesidesymmetric.
Require Export GeoCoq.Elements.OriginalProofs.proposition_07.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_14 : 
   forall A B C D E, 
   RT A B C D B E -> Out B C D -> TS E D B A ->
   Supp A B C D E /\ BetS A B E.
Proof.
(* Goal: forall (A B C D E : @Point Ax0) (_ : @RT Ax0 A B C D B E) (_ : @Out Ax0 B C D) (_ : @TS Ax0 E D B A), and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
intros.
let Tf:=fresh in
assert (Tf:exists a b c d e, (Supp a b c d e /\ CongA A B C a b c /\ CongA D B E d b e)) by (conclude_def RT );destruct Tf as [a[b[c[d[e]]]]];spliter.
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (CongA a b c A B C) by (conclude lemma_equalanglessymmetric).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (CongA d b e D B E) by (conclude lemma_equalanglessymmetric).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (nCol A B C) by (conclude lemma_equalanglesNC).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (neq A B) by (forward_using lemma_NCdistinct).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (nCol D B E) by (conclude lemma_equalanglesNC).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (neq B E) by (forward_using lemma_NCdistinct).
let Tf:=fresh in
assert (Tf:exists T, (BetS A B T /\ Cong B T B E)) by (conclude lemma_extension);destruct Tf as [T];spliter.
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (Cong B D B D) by (conclude cn_congruencereflexive).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (Supp A B C D T) by (conclude_def Supp ).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (CongA a b c A B C) by (conclude lemma_equalanglessymmetric).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (CongA d b e D B E) by (conclude lemma_equalanglessymmetric).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (CongA d b e D B T) by (conclude lemma_supplements).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (CongA D B E D B T) by (conclude lemma_equalanglestransitive).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (CongA D B T D B E) by (conclude lemma_equalanglessymmetric).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (Col A B T) by (conclude_def Col ).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (neq B T) by (forward_using lemma_betweennotequal).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (neq T B) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (Col A B B) by (conclude_def Col ).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (nCol T B C) by (conclude lemma_NChelper).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (nCol C B T) by (forward_using lemma_NCorder).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (Col B C D) by (conclude lemma_rayimpliescollinear).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (Col C B D) by (forward_using lemma_collinearorder).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (neq D B) by (forward_using lemma_NCdistinct).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (Col C B B) by (conclude_def Col ).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (nCol D B T) by (conclude lemma_NChelper).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (Cong D T D E) by (conclude proposition_04).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (Cong T D E D) by (forward_using lemma_congruenceflip).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (Cong T B E B) by (forward_using lemma_congruenceflip).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (Col D B B) by (conclude_def Col ).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (TS A D B E) by (conclude lemma_oppositesidesymmetric).
let Tf:=fresh in
assert (Tf:exists m, (BetS A m E /\ Col D B m /\ nCol D B A)) by (conclude_def TS );destruct Tf as [m];spliter.
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (BetS E m A) by (conclude axiom_betweennesssymmetry).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (BetS T B A) by (conclude axiom_betweennesssymmetry).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (OS T E D B) by (conclude_def OS ).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (neq B C) by (forward_using lemma_NCdistinct).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (neq C B) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (eq T E) by (conclude proposition_07).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (BetS A B E) by (conclude cn_equalitysub).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
assert (Supp A B C D E) by (conclude_def Supp ).
(* Goal: and (@Supp Ax0 A B C D E) (@BetS Ax0 A B E) *)
close.
Qed.

End Euclid.


