Require Export GeoCoq.Elements.OriginalProofs.lemma_betweennotequal.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_lessthannotequal : 
   forall A B C D, 
   Lt A B C D ->
   neq A B /\ neq C D.
Proof.
(* Goal: forall (A B C D : @Point Ax1) (_ : @Lt Ax1 A B C D), and (@neq Ax1 A B) (@neq Ax1 C D) *)
intros.
let Tf:=fresh in
assert (Tf:exists E, (BetS C E D /\ Cong C E A B)) by (conclude_def Lt );destruct Tf as [E];spliter.
(* Goal: and (@neq Ax1 A B) (@neq Ax1 C D) *)
assert (neq C E) by (forward_using lemma_betweennotequal).
(* Goal: and (@neq Ax1 A B) (@neq Ax1 C D) *)
assert (neq A B) by (conclude axiom_nocollapse).
(* Goal: and (@neq Ax1 A B) (@neq Ax1 C D) *)
assert (neq C D) by (forward_using lemma_betweennotequal).
(* Goal: and (@neq Ax1 A B) (@neq Ax1 C D) *)
close.
Qed.

End Euclid.


