Library GeoCoq.Elements.OriginalProofs.lemma_partnotequalwhole

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

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_partnotequalwhole :
   ∀ A B C,
   BetS A B C →
   ¬ Cong A B A C.
Proof.
intros.
assert (neq A B) by (forward_using lemma_betweennotequal).
assert (neq B A) by (conclude lemma_inequalitysymmetric).
let Tf:=fresh in
assert (Tf:∃ D, (BetS B A D ∧ Cong A D B A)) by (conclude postulate_extension);destruct Tf as [D];spliter.
assert (BetS D A B) by (conclude axiom_betweennesssymmetry).
assert (BetS D A C) by (conclude lemma_3_7b).
assert (neq B C) by (forward_using lemma_betweennotequal).
assert (neq D A) by (forward_using lemma_betweennotequal).
assert (¬ Cong A B A C).
 {
 intro.
 assert (eq B C) by (conclude lemma_extensionunique).
 contradict.
 }
close.
Qed.

End Euclid.