Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NCorder.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NChelper.
Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglesreflexive.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma proposition_13 : 
   forall A B C D, 
   BetS D B C -> nCol A B C ->
   RT C B A A B D.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @BetS Ax0 D B C) (_ : @nCol Ax0 A B C), @RT Ax0 C B A A B D *)
intros.
(* Goal: @RT Ax0 C B A A B D *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @RT Ax0 C B A A B D *)
assert (neq B A) by (forward_using lemma_NCdistinct).
(* Goal: @RT Ax0 C B A A B D *)
assert (Out B A A) by (conclude lemma_ray4).
(* Goal: @RT Ax0 C B A A B D *)
assert (BetS C B D) by (conclude axiom_betweennesssymmetry).
(* Goal: @RT Ax0 C B A A B D *)
assert (Supp C B A A D) by (conclude_def Supp ).
(* Goal: @RT Ax0 C B A A B D *)
assert (nCol C B A) by (forward_using lemma_NCorder).
(* Goal: @RT Ax0 C B A A B D *)
assert (Col D B C) by (conclude_def Col ).
(* Goal: @RT Ax0 C B A A B D *)
assert (Col C B D) by (forward_using lemma_collinearorder).
(* Goal: @RT Ax0 C B A A B D *)
assert (eq B B) by (conclude cn_equalityreflexive).
(* Goal: @RT Ax0 C B A A B D *)
assert (Col C B B) by (conclude_def Col ).
(* Goal: @RT Ax0 C B A A B D *)
assert (neq D B) by (forward_using lemma_betweennotequal).
(* Goal: @RT Ax0 C B A A B D *)
assert (nCol D B A) by (conclude lemma_NChelper).
(* Goal: @RT Ax0 C B A A B D *)
assert (nCol A B D) by (forward_using lemma_NCorder).
(* Goal: @RT Ax0 C B A A B D *)
assert (CongA A B D A B D) by (conclude lemma_equalanglesreflexive).
(* Goal: @RT Ax0 C B A A B D *)
assert (CongA C B A C B A) by (conclude lemma_equalanglesreflexive).
(* Goal: @RT Ax0 C B A A B D *)
assert (RT C B A A B D) by (conclude_def RT ).
(* Goal: @RT Ax0 C B A A B D *)
close.
Qed.

End Euclid.