Library GeoCoq.Elements.OriginalProofs.lemma_collinear5

Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear4.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_collinear5 :
   ∀ A B C D E,
   neq A B → neq C D → Col A B C → Col A B D → Col A B E →
   Col C D E.
Proof.
intros.
assert (Col B C D) by (conclude lemma_collinear4).
assert (Col B C E) by (conclude lemma_collinear4).
assert (Col C D E).
by cases on (neq B C ∨ eq B C).
{
 assert (Col C D E) by (conclude lemma_collinear4).
 close.
 }
{
 assert (Col B D E) by (conclude lemma_collinear4).
 assert (Col C D E) by (conclude cn_equalitysub).
 close.
 }

close.
Qed.

End Euclid.