Require Export GeoCoq.Elements.OriginalProofs.lemma_collinearorder.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_NCorder : 
   forall A B C, 
   nCol A B C ->
   nCol B A C /\ nCol B C A /\ nCol C A B /\ nCol A C B /\ nCol C B A.
Proof.
(* Goal: forall (A B C : @Point Ax1) (_ : @nCol Ax1 A B C), and (@nCol Ax1 B A C) (and (@nCol Ax1 B C A) (and (@nCol Ax1 C A B) (and (@nCol Ax1 A C B) (@nCol Ax1 C B A)))) *)
intros.
(* Goal: and (@nCol Ax1 B A C) (and (@nCol Ax1 B C A) (and (@nCol Ax1 C A B) (and (@nCol Ax1 A C B) (@nCol Ax1 C B A)))) *)
assert (~ Col B A C).
(* Goal: not (@Col Ax1 C B A) *)
(* Goal: and (@nCol Ax1 B A C) (and (@nCol Ax1 B C A) (and (@nCol Ax1 C A B) (and (@nCol Ax1 A C B) (@nCol Ax1 C B A)))) *)
 {
(* Goal: not (@Col Ax1 C B A) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@nCol Ax1 B A C) (and (@nCol Ax1 B C A) (and (@nCol Ax1 C A B) (and (@nCol Ax1 A C B) (@nCol Ax1 C B A)))) *)
assert (~ Col B C A).
(* Goal: not (@Col Ax1 C B A) *)
(* Goal: and (@nCol Ax1 B A C) (and (@nCol Ax1 B C A) (and (@nCol Ax1 C A B) (and (@nCol Ax1 A C B) (@nCol Ax1 C B A)))) *)
 {
(* Goal: not (@Col Ax1 C B A) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@nCol Ax1 B A C) (and (@nCol Ax1 B C A) (and (@nCol Ax1 C A B) (and (@nCol Ax1 A C B) (@nCol Ax1 C B A)))) *)
assert (~ Col C A B).
(* Goal: not (@Col Ax1 C B A) *)
(* Goal: and (@nCol Ax1 B A C) (and (@nCol Ax1 B C A) (and (@nCol Ax1 C A B) (and (@nCol Ax1 A C B) (@nCol Ax1 C B A)))) *)
 {
(* Goal: not (@Col Ax1 C B A) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@nCol Ax1 B A C) (and (@nCol Ax1 B C A) (and (@nCol Ax1 C A B) (and (@nCol Ax1 A C B) (@nCol Ax1 C B A)))) *)
assert (~ Col A C B).
(* Goal: not (@Col Ax1 C B A) *)
(* Goal: and (@nCol Ax1 B A C) (and (@nCol Ax1 B C A) (and (@nCol Ax1 C A B) (and (@nCol Ax1 A C B) (@nCol Ax1 C B A)))) *)
 {
(* Goal: not (@Col Ax1 C B A) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@nCol Ax1 B A C) (and (@nCol Ax1 B C A) (and (@nCol Ax1 C A B) (and (@nCol Ax1 A C B) (@nCol Ax1 C B A)))) *)
assert (~ Col C B A).
(* Goal: not (@Col Ax1 C B A) *)
(* Goal: and (@nCol Ax1 B A C) (and (@nCol Ax1 B C A) (and (@nCol Ax1 C A B) (and (@nCol Ax1 A C B) (@nCol Ax1 C B A)))) *)
 {
(* Goal: not (@Col Ax1 C B A) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (forward_using lemma_collinearorder).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@nCol Ax1 B A C) (and (@nCol Ax1 B C A) (and (@nCol Ax1 C A B) (and (@nCol Ax1 A C B) (@nCol Ax1 C B A)))) *)
close.
Qed.

End Euclid.


