Require Export GeoCoq.Elements.OriginalProofs.lemma_inequalitysymmetric.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

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

End Euclid.


