Require Export GeoCoq.Elements.OriginalProofs.lemma_planeseparation.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_samesidetransitive : 
   forall A B P Q R, 
   OS P Q A B -> OS Q R A B ->
   OS P R A B.
Proof.
(* Goal: forall (A B P Q R : @Point Ax) (_ : @OS Ax P Q A B) (_ : @OS Ax Q R A B), @OS Ax P R A B *)
intros.
let Tf:=fresh in
assert (Tf:exists E F G, (Col A B E /\ Col A B F /\ BetS Q E G /\ BetS R F G /\ nCol A B Q /\ nCol A B R)) by (conclude_def OS );destruct Tf as [E[F[G]]];spliter.
(* Goal: @OS Ax P R A B *)
assert (TS Q A B G) by (conclude_def TS ).
(* Goal: @OS Ax P R A B *)
assert (TS P A B G) by (conclude lemma_planeseparation).
let Tf:=fresh in
assert (Tf:exists M, (BetS P M G /\ Col A B M /\ nCol A B P)) by (conclude_def TS );destruct Tf as [M];spliter.
(* Goal: @OS Ax P R A B *)
assert (OS P R A B) by (conclude_def OS ).
(* Goal: @OS Ax P R A B *)
close.
Qed.

End Euclid.


