Require Export GeoCoq.Elements.OriginalProofs.lemma_samesidesymmetric.
Require Export GeoCoq.Elements.OriginalProofs.lemma_planeseparation.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_samenotopposite : 
   forall A B C D, 
   OS A B C D ->
   ~ TS A C D B.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @OS Ax0 A B C D), not (@TS Ax0 A C D B) *)
intros.
(* Goal: not (@TS Ax0 A C D B) *)
assert (OS B A C D) by (forward_using lemma_samesidesymmetric).
(* Goal: not (@TS Ax0 A C D B) *)
assert (~ TS A C D B).
(* Goal: not (@TS Ax0 A C D B) *)
(* Goal: not (@TS Ax0 A C D B) *)
 {
(* Goal: not (@TS Ax0 A C D B) *)
 intro.
(* Goal: False *)
 assert (TS B C D B) by (conclude lemma_planeseparation).
 let Tf:=fresh in
 assert (Tf:exists M, BetS B M B) by (conclude_def TS );destruct Tf as [M];spliter.
(* Goal: False *)
 assert (~ BetS B M B) by (conclude axiom_betweennessidentity).
(* Goal: False *)
 contradict.
 }
(* Goal: not (@TS Ax0 A C D B) *)
close.
Qed.

End Euclid.


