Library GeoCoq.Elements.OriginalProofs.lemma_samesideflip

Require Export GeoCoq.Elements.OriginalProofs.lemma_NCorder.

Section Euclid.

Context `{Ax1:euclidean_neutral}.

Lemma lemma_samesideflip :
   ∀ A B P Q,
   OS P Q A B →
   OS P Q B A.
Proof.
intros.
let Tf:=fresh in
assert (Tf:∃ 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.
assert (Col B A p) by (forward_using lemma_collinearorder).
assert (Col B A q) by (forward_using lemma_collinearorder).
assert (nCol B A P) by (forward_using lemma_NCorder).
assert (nCol B A Q) by (forward_using lemma_NCorder).
assert (OS P Q B A) by (conclude_def OS ).
close.
Qed.

End Euclid.