Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_collinear1.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_collinearorder : 
   forall A B C, 
   Col A B C ->
   Col B A C /\ Col B C A /\ Col C A B /\ Col A C B /\ Col C B A.
Proof.
(* Goal: forall (A B C : @Point Ax1) (_ : @Col Ax1 A B C), and (@Col Ax1 B A C) (and (@Col Ax1 B C A) (and (@Col Ax1 C A B) (and (@Col Ax1 A C B) (@Col Ax1 C B A)))) *)
intros.
(* Goal: and (@Col Ax1 B A C) (and (@Col Ax1 B C A) (and (@Col Ax1 C A B) (and (@Col Ax1 A C B) (@Col Ax1 C B A)))) *)
assert (Col B C A) by (conclude lemma_collinear2).
(* Goal: and (@Col Ax1 B A C) (and (@Col Ax1 B C A) (and (@Col Ax1 C A B) (and (@Col Ax1 A C B) (@Col Ax1 C B A)))) *)
assert (Col C A B) by (conclude lemma_collinear2).
(* Goal: and (@Col Ax1 B A C) (and (@Col Ax1 B C A) (and (@Col Ax1 C A B) (and (@Col Ax1 A C B) (@Col Ax1 C B A)))) *)
assert (Col B A C) by (conclude lemma_collinear1).
(* Goal: and (@Col Ax1 B A C) (and (@Col Ax1 B C A) (and (@Col Ax1 C A B) (and (@Col Ax1 A C B) (@Col Ax1 C B A)))) *)
assert (Col A C B) by (conclude lemma_collinear2).
(* Goal: and (@Col Ax1 B A C) (and (@Col Ax1 B C A) (and (@Col Ax1 C A B) (and (@Col Ax1 A C B) (@Col Ax1 C B A)))) *)
assert (Col C B A) by (conclude lemma_collinear2).
(* Goal: and (@Col Ax1 B A C) (and (@Col Ax1 B C A) (and (@Col Ax1 C A B) (and (@Col Ax1 A C B) (@Col Ax1 C B A)))) *)
close.
Qed.

End Euclid.


