# Library GeoCoq.Elements.OriginalProofs.proposition_13

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 :

∀ A B C D,

BetS D B C → nCol A B C →

RT C B A A B D.

Proof.

intros.

assert (eq A A) by (conclude cn_equalityreflexive).

assert (neq B A) by (forward_using lemma_NCdistinct).

assert (Out B A A) by (conclude lemma_ray4).

assert (BetS C B D) by (conclude axiom_betweennesssymmetry).

assert (Supp C B A A D) by (conclude_def Supp ).

assert (nCol C B A) by (forward_using lemma_NCorder).

assert (Col D B C) by (conclude_def Col ).

assert (Col C B D) by (forward_using lemma_collinearorder).

assert (eq B B) by (conclude cn_equalityreflexive).

assert (Col C B B) by (conclude_def Col ).

assert (neq D B) by (forward_using lemma_betweennotequal).

assert (nCol D B A) by (conclude lemma_NChelper).

assert (nCol A B D) by (forward_using lemma_NCorder).

assert (CongA A B D A B D) by (conclude lemma_equalanglesreflexive).

assert (CongA C B A C B A) by (conclude lemma_equalanglesreflexive).

assert (RT C B A A B D) by (conclude_def RT ).

close.

Qed.

End Euclid.

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 :

∀ A B C D,

BetS D B C → nCol A B C →

RT C B A A B D.

Proof.

intros.

assert (eq A A) by (conclude cn_equalityreflexive).

assert (neq B A) by (forward_using lemma_NCdistinct).

assert (Out B A A) by (conclude lemma_ray4).

assert (BetS C B D) by (conclude axiom_betweennesssymmetry).

assert (Supp C B A A D) by (conclude_def Supp ).

assert (nCol C B A) by (forward_using lemma_NCorder).

assert (Col D B C) by (conclude_def Col ).

assert (Col C B D) by (forward_using lemma_collinearorder).

assert (eq B B) by (conclude cn_equalityreflexive).

assert (Col C B B) by (conclude_def Col ).

assert (neq D B) by (forward_using lemma_betweennotequal).

assert (nCol D B A) by (conclude lemma_NChelper).

assert (nCol A B D) by (forward_using lemma_NCorder).

assert (CongA A B D A B D) by (conclude lemma_equalanglesreflexive).

assert (CongA C B A C B A) by (conclude lemma_equalanglesreflexive).

assert (RT C B A A B D) by (conclude_def RT ).

close.

Qed.

End Euclid.