Library GeoCoq.Elements.OriginalProofs.lemma_collinear2

Require Export GeoCoq.Elements.OriginalProofs.lemma_equalitysymmetric.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_collinear2 :
   ∀ A B C,
   Col A B C →
   Col B C A.
Proof.
intros.
assert ((eq A B ∨ eq A C ∨ eq B C ∨ BetS B A C ∨ BetS A B C ∨ BetS A C B)) by (conclude_def Col ).
assert (Col B C A).
by cases on (eq A B ∨ eq A C ∨ eq B C ∨ BetS B A C ∨ BetS A B C ∨ BetS A C B).
{
 assert (eq B A) by (conclude lemma_equalitysymmetric).
 assert (Col B C A) by (conclude_def Col ).
 close.
 }
{
 assert (eq C A) by (conclude lemma_equalitysymmetric).
 assert (Col B C A) by (conclude_def Col ).
 close.
 }
{
 assert (Col B C A) by (conclude_def Col ).
 close.
 }
{
 assert (Col B C A) by (conclude_def Col ).
 close.
 }
{
 assert (BetS C B A) by (conclude axiom_betweennesssymmetry).
 assert (Col B C A) by (conclude_def Col ).
 close.
 }
{
 assert (BetS B C A) by (conclude axiom_betweennesssymmetry).
 assert (Col B C A) by (conclude_def Col ).
 close.
 }

close.
Qed.

End Euclid.