Require Export GeoCoq.Elements.OriginalProofs.lemma_NCorder.

Section Euclid.

Context `{Ax:euclidean_neutral}.

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

End Euclid.


