Require Export GeoCoq.Elements.OriginalProofs.lemma_equalanglessymmetric.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_angledistinct : 
   forall A B C a b c, 
   CongA A B C a b c ->
   neq A B /\ neq B C /\ neq A C /\ neq a b /\ neq b c /\ neq a c.
Proof.
(* Goal: forall (A B C a b c : @Point Ax) (_ : @CongA Ax A B C a b c), and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
intros.
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
assert (nCol A B C) by (conclude_def CongA ).
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
assert (~ eq A B).
(* Goal: not (@eq Ax a c) *)
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
 {
(* Goal: not (@eq Ax a c) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
assert (~ eq B C).
(* Goal: not (@eq Ax a c) *)
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
 {
(* Goal: not (@eq Ax a c) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
assert (~ eq A C).
(* Goal: not (@eq Ax a c) *)
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
 {
(* Goal: not (@eq Ax a c) *)
 intro.
(* Goal: False *)
 assert (Col A B C) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
assert (CongA a b c A B C) by (conclude lemma_equalanglessymmetric).
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
assert (nCol a b c) by (conclude_def CongA ).
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
assert (~ eq a b).
(* Goal: not (@eq Ax a c) *)
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
 {
(* Goal: not (@eq Ax a c) *)
 intro.
(* Goal: False *)
 assert (Col a b c) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
assert (~ eq b c).
(* Goal: not (@eq Ax a c) *)
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
 {
(* Goal: not (@eq Ax a c) *)
 intro.
(* Goal: False *)
 assert (Col a b c) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
assert (~ eq a c).
(* Goal: not (@eq Ax a c) *)
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
 {
(* Goal: not (@eq Ax a c) *)
 intro.
(* Goal: False *)
 assert (Col a b c) by (conclude_def Col ).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@neq Ax A B) (and (@neq Ax B C) (and (@neq Ax A C) (and (@neq Ax a b) (and (@neq Ax b c) (@neq Ax a c))))) *)
close.
Qed.

End Euclid.


