Require Export GeoCoq.Elements.OriginalProofs.lemma_NCorder.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_samesideflip : 
   forall A B P Q, 
   OS P Q A B ->
   OS P Q B A.
Proof.
(* Goal: forall (A B P Q : @Point Ax1) (_ : @OS Ax1 P Q A B), @OS Ax1 P Q B A *)
intros.
let Tf:=fresh in
assert (Tf:exists p q r, (Col A B p /\ Col A B q /\ BetS P p r /\ BetS Q q r /\ nCol A B P /\ nCol A B Q)) by (conclude_def OS );destruct Tf as [p[q[r]]];spliter.
(* Goal: @OS Ax1 P Q B A *)
assert (Col B A p) by (forward_using lemma_collinearorder).
(* Goal: @OS Ax1 P Q B A *)
assert (Col B A q) by (forward_using lemma_collinearorder).
(* Goal: @OS Ax1 P Q B A *)
assert (nCol B A P) by (forward_using lemma_NCorder).
(* Goal: @OS Ax1 P Q B A *)
assert (nCol B A Q) by (forward_using lemma_NCorder).
(* Goal: @OS Ax1 P Q B A *)
assert (OS P Q B A) by (conclude_def OS ).
(* Goal: @OS Ax1 P Q B A *)
close.
Qed.

End Euclid.


