Require Export GeoCoq.Elements.OriginalProofs.lemma_3_6a.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_betweennotequal : 
   forall A B C, 
   BetS A B C ->
   neq B C /\ neq A B /\ neq A C.
Proof.
(* Goal: forall (A B C : @Point Ax) (_ : @BetS Ax A B C), and (@neq Ax B C) (and (@neq Ax A B) (@neq Ax A C)) *)
intros.
(* Goal: and (@neq Ax B C) (and (@neq Ax A B) (@neq Ax A C)) *)
assert (~ eq B C).
(* Goal: not (@eq Ax A C) *)
(* Goal: and (@neq Ax B C) (and (@neq Ax A B) (@neq Ax A C)) *)
 {
(* Goal: not (@eq Ax A C) *)
 intro.
(* Goal: False *)
 assert (BetS A C B) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (BetS B C B) by (conclude lemma_3_6a).
(* Goal: False *)
 assert (~ BetS B C B) by (conclude axiom_betweennessidentity).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@neq Ax B C) (and (@neq Ax A B) (@neq Ax A C)) *)
assert (~ eq A B).
(* Goal: not (@eq Ax A C) *)
(* Goal: and (@neq Ax B C) (and (@neq Ax A B) (@neq Ax A C)) *)
 {
(* Goal: not (@eq Ax A C) *)
 intro.
(* Goal: False *)
 assert (BetS B A C) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (BetS A B A) by (conclude axiom_innertransitivity).
(* Goal: False *)
 assert (~ BetS A B A) by (conclude axiom_betweennessidentity).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@neq Ax B C) (and (@neq Ax A B) (@neq Ax A C)) *)
assert (~ eq A C).
(* Goal: not (@eq Ax A C) *)
(* Goal: and (@neq Ax B C) (and (@neq Ax A B) (@neq Ax A C)) *)
 {
(* Goal: not (@eq Ax A C) *)
 intro.
(* Goal: False *)
 assert (BetS A B A) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (~ BetS A B A) by (conclude axiom_betweennessidentity).
(* Goal: False *)
 contradict.
 }
(* Goal: and (@neq Ax B C) (and (@neq Ax A B) (@neq Ax A C)) *)
close.
Qed.

End Euclid.


