Library GeoCoq.Elements.OriginalProofs.lemma_ray1

Require Export GeoCoq.Elements.OriginalProofs.lemma_ray.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_ray1 :
   ∀ A B P,
   Out A B P →
   (BetS A P B ∨ eq B P ∨ BetS A B P).
Proof.
intros.
assert (¬ ¬ (BetS A P B ∨ eq B P ∨ BetS A B P)).
 {
 intro.
 assert (neq P B) by (conclude lemma_inequalitysymmetric).
 assert (BetS A B P) by (conclude lemma_ray).
 contradict.
 }
close.
Qed.

End Euclid.