Require Export GeoCoq.Elements.OriginalProofs.lemma_ray2.
Require Export GeoCoq.Elements.OriginalProofs.lemma_lessthancongruence.
Require Export GeoCoq.Elements.OriginalProofs.lemma_3_7b.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_ray : 
   forall A B P, 
   Out A B P -> neq P B -> ~ BetS A P B ->
   BetS A B P.
Proof.
(* Goal: forall (A B P : @Point Ax0) (_ : @Out Ax0 A B P) (_ : @neq Ax0 P B) (_ : not (@BetS Ax0 A P B)), @BetS Ax0 A B P *)
intros.
(* Goal: @BetS Ax0 A B P *)
assert (neq A B) by (conclude lemma_ray2).
let Tf:=fresh in
assert (Tf:exists E, (BetS E A P /\ BetS E A B)) by (conclude_def Out );destruct Tf as [E];spliter.
(* Goal: @BetS Ax0 A B P *)
assert (neq A P) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists D, (BetS A B D /\ Cong B D A P)) by (conclude lemma_extension);destruct Tf as [D];spliter.
(* Goal: @BetS Ax0 A B P *)
assert (Cong D B B D) by (conclude cn_equalityreverse).
(* Goal: @BetS Ax0 A B P *)
assert (Cong D B A P) by (conclude lemma_congruencetransitive).
(* Goal: @BetS Ax0 A B P *)
assert (BetS D B A) by (conclude axiom_betweennesssymmetry).
(* Goal: @BetS Ax0 A B P *)
assert (Lt A P D A) by (conclude_def Lt ).
(* Goal: @BetS Ax0 A B P *)
assert (Cong D A A D) by (conclude cn_equalityreverse).
(* Goal: @BetS Ax0 A B P *)
assert (Lt A P A D) by (conclude lemma_lessthancongruence).
let Tf:=fresh in
assert (Tf:exists F, (BetS A F D /\ Cong A F A P)) by (conclude_def Lt );destruct Tf as [F];spliter.
(* Goal: @BetS Ax0 A B P *)
assert (BetS E A D) by (conclude lemma_3_7b).
(* Goal: @BetS Ax0 A B P *)
assert (BetS E A F) by (conclude axiom_innertransitivity).
(* Goal: @BetS Ax0 A B P *)
assert (Cong A P A F) by (conclude lemma_congruencesymmetric).
(* Goal: @BetS Ax0 A B P *)
assert (eq P F) by (conclude lemma_extensionunique).
(* Goal: @BetS Ax0 A B P *)
assert (BetS A P D) by (conclude cn_equalitysub).
(* Goal: @BetS Ax0 A B P *)
assert (~ ~ BetS A B P).
(* Goal: not (not (@BetS Ax0 A B P)) *)
(* Goal: @BetS Ax0 A B P *)
 {
(* Goal: not (not (@BetS Ax0 A B P)) *)
 intro.
(* Goal: False *)
 assert (eq B P) by (conclude axiom_connectivity).
(* Goal: False *)
 assert (neq B P) by (conclude lemma_inequalitysymmetric).
(* Goal: False *)
 contradict.
 }
(* Goal: @BetS Ax0 A B P *)
close.
Qed.

End Euclid.


