Require Export GeoCoq.Elements.OriginalProofs.lemma_ray.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_ray1 : 
   forall A B P, 
   Out A B P ->
   (BetS A P B \/ eq B P \/ BetS A B P).
Proof.
(* Goal: forall (A B P : @Point Ax0) (_ : @Out Ax0 A B P), or (@BetS Ax0 A P B) (or (@eq Ax0 B P) (@BetS Ax0 A B P)) *)
intros.
(* Goal: or (@BetS Ax0 A P B) (or (@eq Ax0 B P) (@BetS Ax0 A B P)) *)
assert (~ ~ (BetS A P B \/ eq B P \/ BetS A B P)).
(* Goal: not (not (or (@BetS Ax0 A P B) (or (@eq Ax0 B P) (@BetS Ax0 A B P)))) *)
(* Goal: or (@BetS Ax0 A P B) (or (@eq Ax0 B P) (@BetS Ax0 A B P)) *)
 {
(* Goal: not (not (or (@BetS Ax0 A P B) (or (@eq Ax0 B P) (@BetS Ax0 A B P)))) *)
 intro.
(* Goal: False *)
 assert (neq P B) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 assert (BetS A B P) by (conclude lemma_ray).
(* Goal: False *)
 contradict.
 }
(* Goal: or (@BetS Ax0 A P B) (or (@eq Ax0 B P) (@BetS Ax0 A B P)) *)
close.
Qed.

End Euclid.


