Require Export GeoCoq.Elements.OriginalProofs.lemma_NCdistinct.
Require Export GeoCoq.Elements.OriginalProofs.lemma_NChelper.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_samesidecollinear : 
   forall A B C P Q, 
   OS P Q A B -> Col A B C -> neq A C ->
   OS P Q A C.
Proof.
(* Goal: forall (A B C P Q : @Point Ax) (_ : @OS Ax P Q A B) (_ : @Col Ax A B C) (_ : @neq Ax A C), @OS Ax P Q A C *)
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 Ax P Q A C *)
assert (neq A B) by (forward_using lemma_NCdistinct).
(* Goal: @OS Ax P Q A C *)
assert (eq A A) by (conclude cn_equalityreflexive).
(* Goal: @OS Ax P Q A C *)
assert (Col A B A) by (conclude_def Col ).
(* Goal: @OS Ax P Q A C *)
assert (nCol A C P) by (conclude lemma_NChelper).
(* Goal: @OS Ax P Q A C *)
assert (nCol A C Q) by (conclude lemma_NChelper).
(* Goal: @OS Ax P Q A C *)
assert (Col B A p) by (forward_using lemma_collinearorder).
(* Goal: @OS Ax P Q A C *)
assert (Col B A C) by (forward_using lemma_collinearorder).
(* Goal: @OS Ax P Q A C *)
assert (neq B A) by (conclude lemma_inequalitysymmetric).
(* Goal: @OS Ax P Q A C *)
assert (Col A C p) by (conclude lemma_collinear4).
(* Goal: @OS Ax P Q A C *)
assert (Col B A q) by (forward_using lemma_collinearorder).
(* Goal: @OS Ax P Q A C *)
assert (Col A C q) by (conclude lemma_collinear4).
(* Goal: @OS Ax P Q A C *)
assert (OS P Q A C) by (conclude_def OS ).
(* Goal: @OS Ax P Q A C *)
close.
Qed.

End Euclid.


