# 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.

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.