Library GeoCoq.Elements.OriginalProofs.lemma_lessthannotequal

Require Export GeoCoq.Elements.OriginalProofs.lemma_betweennotequal.
Require Export GeoCoq.Elements.OriginalProofs.lemma_nullsegment3.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_lessthannotequal :
   ∀ A B C D,
   Lt A B C D →
   neq A B ∧ neq C D.
Proof.
intros.
let Tf:=fresh in
assert (Tf:∃ E, (BetS C E D ∧ Cong C E A B)) by (conclude_def Lt );destruct Tf as [E];spliter.
assert (neq C E) by (forward_using lemma_betweennotequal).
assert (neq A B) by (conclude lemma_nullsegment3).
assert (neq C D) by (forward_using lemma_betweennotequal).
close.
Qed.

End Euclid.