Library GeoCoq.Elements.OriginalProofs.lemma_ray

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

Lemma lemma_ray :
   ∀ A B P,
   Out A B P → neq P B → ¬ BetS A P B →
   BetS A B P.
Proof.
intros.
assert (neq A B) by (conclude lemma_ray2).
let Tf:=fresh in
assert (Tf:∃ E, (BetS E A P ∧ BetS E A B)) by (conclude_def Out );destruct Tf as [E];spliter.
assert (neq A P) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:∃ D, (BetS A B D ∧ Cong B D A P)) by (conclude postulate_extension);destruct Tf as [D];spliter.
assert (Cong A D D A) by (conclude cn_equalityreverse).
assert (Cong D B B D) by (conclude cn_equalityreverse).
assert (Cong D B A P) by (conclude lemma_congruencetransitive).
assert (Cong A P D B) by (conclude lemma_congruencesymmetric).
assert (BetS D B A) by (conclude axiom_betweennesssymmetry).
assert (Lt A P D A) by (conclude_def Lt ).
assert (Cong D A A D) by (conclude cn_equalityreverse).
assert (Lt A P A D) by (conclude lemma_lessthancongruence).
assert (neq A D) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:∃ F, (BetS A F D ∧ Cong A F A P)) by (conclude_def Lt );destruct Tf as [F];spliter.
assert (BetS E A D) by (conclude lemma_3_7b).
assert (BetS E A F) by (conclude axiom_innertransitivity).
assert (Cong A P A F) by (conclude lemma_congruencesymmetric).
assert (neq E A) by (forward_using lemma_betweennotequal).
assert (eq P F) by (conclude lemma_extensionunique).
assert (BetS A P D) by (conclude cn_equalitysub).
assert (BetS E A F) by (conclude axiom_innertransitivity).
assert (¬ ¬ BetS A B P).
 {
 intro.
 assert (eq B P) by (conclude axiom_connectivity).
 assert (neq B P) by (conclude lemma_inequalitysymmetric).
 contradict.
 }
close.
Qed.

End Euclid.