Library GeoCoq.Elements.OriginalProofs.lemma_samesidetransitive

Require Export GeoCoq.Elements.OriginalProofs.lemma_planeseparation.

Section Euclid.

Context `{Ax1:euclidean_neutral_ruler_compass}.

Lemma lemma_samesidetransitive :
   ∀ A B P Q R,
   OS P Q A B → OS Q R A B →
   OS P R A B.
Proof.
intros.
let Tf:=fresh in
assert (Tf:∃ 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.
assert (TS Q A B G) by (conclude_def TS ).
assert (TS P A B G) by (conclude lemma_planeseparation).
let Tf:=fresh in
assert (Tf:∃ M, (BetS P M G ∧ Col A B M ∧ nCol A B P)) by (conclude_def TS );destruct Tf as [M];spliter.
assert (OS P R A B) by (conclude_def OS ).
close.
Qed.

End Euclid.