Require Export GeoCoq.Elements.OriginalProofs.lemma_inequalitysymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_3_7b.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_partnotequalwhole : 
   forall A B C, 
   BetS A B C ->
   ~ Cong A B A C.
Proof.
(* Goal: forall (A B C : @Point Ax0) (_ : @BetS Ax0 A B C), not (@Cong Ax0 A B A C) *)
intros.
(* Goal: not (@Cong Ax0 A B A C) *)
assert (neq A B) by (forward_using lemma_betweennotequal).
(* Goal: not (@Cong Ax0 A B A C) *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:exists D, BetS B A D) by (conclude postulate_Euclid2);destruct Tf as [D];spliter.
(* Goal: not (@Cong Ax0 A B A C) *)
assert (BetS D A B) by (conclude axiom_betweennesssymmetry).
(* Goal: not (@Cong Ax0 A B A C) *)
assert (BetS D A C) by (conclude lemma_3_7b).
(* Goal: not (@Cong Ax0 A B A C) *)
assert (neq B C) by (forward_using lemma_betweennotequal).
(* Goal: not (@Cong Ax0 A B A C) *)
assert (~ Cong A B A C).
(* Goal: not (@Cong Ax0 A B A C) *)
(* Goal: not (@Cong Ax0 A B A C) *)
 {
(* Goal: not (@Cong Ax0 A B A C) *)
 intro.
(* Goal: False *)
 assert (eq B C) by (conclude lemma_extensionunique).
(* Goal: False *)
 contradict.
 }
(* Goal: not (@Cong Ax0 A B A C) *)
close.
Qed.

End Euclid.


