Require Export GeoCoq.Elements.OriginalProofs.lemma_equalitysymmetric.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_inequalitysymmetric : 
   forall A B, 
   neq A B ->
   neq B A.
Proof.
(* Goal: forall (A B : @Point Ax) (_ : @neq Ax A B), @neq Ax B A *)
intros.
(* Goal: @neq Ax B A *)
assert (~ eq B A).
(* Goal: not (@eq Ax B A) *)
(* Goal: @neq Ax B A *)
 {
(* Goal: not (@eq Ax B A) *)
 intro.
(* Goal: False *)
 assert (eq A B) by (conclude lemma_equalitysymmetric).
(* Goal: False *)
 contradict.
 }
(* Goal: @neq Ax B A *)
close.
Qed.

End Euclid.
