Require Export GeoCoq.Elements.OriginalProofs.lemma_Euclid4.
Require Export GeoCoq.Elements.OriginalProofs.proposition_14.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_righttogether : 
   forall A B C G, 
   Per G A B -> Per B A C -> TS G B A C ->
   RT G A B B A C /\ BetS G A C.
Proof.
(* Goal: forall (A B C G : @Point Ax0) (_ : @Per Ax0 G A B) (_ : @Per Ax0 B A C) (_ : @TS Ax0 G B A C), and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
intros.
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (Per B A G) by (conclude lemma_8_2).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (neq A G) by (conclude_def Per ).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (neq G A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists D, (BetS G A D /\ Cong A D G A)) by (conclude lemma_extension);destruct Tf as [D];spliter.
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (neq A B) by (conclude_def Per ).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (Out A B B) by (conclude lemma_ray4).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (Supp G A B B D) by (conclude_def Supp ).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (nCol B A G) by (conclude_def TS ).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (nCol G A B) by (forward_using lemma_NCorder).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (CongA G A B G A B) by (conclude lemma_equalanglesreflexive).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (Col G A D) by (conclude_def Col ).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (neq A D) by (forward_using lemma_betweennotequal).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (neq D A) by (conclude lemma_inequalitysymmetric).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (Per D A B) by (conclude lemma_collinearright).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (Per B A D) by (conclude lemma_8_2).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (CongA B A C B A D) by (conclude lemma_Euclid4).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (RT G A B B A C) by (conclude_def RT ).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (TS C B A G) by (conclude lemma_oppositesidesymmetric).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
assert (BetS G A C) by (conclude proposition_14).
(* Goal: and (@RT Ax0 G A B B A C) (@BetS Ax0 G A C) *)
close.
Qed.

End Euclid.


