Require Export GeoCoq.Elements.OriginalProofs.lemma_extension.
Require Export GeoCoq.Elements.OriginalProofs.lemma_3_6b.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

Lemma lemma_outerconnectivity : 
   forall A B C D, 
   BetS A B C -> BetS A B D -> ~ BetS B C D -> ~ BetS B D C ->
   eq C D.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @BetS Ax0 A B C) (_ : @BetS Ax0 A B D) (_ : not (@BetS Ax0 B C D)) (_ : not (@BetS Ax0 B D C)), @eq Ax0 C D *)
intros.
(* Goal: @eq Ax0 C D *)
assert (~ eq A C).
(* Goal: not (@eq Ax0 A D) *)
(* Goal: @eq Ax0 C D *)
 {
(* Goal: not (@eq Ax0 A D) *)
 intro.
(* Goal: False *)
 assert (BetS A B A) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (~ BetS A B A) by (conclude axiom_betweennessidentity).
(* Goal: False *)
 contradict.
 }
(* Goal: @eq Ax0 C D *)
assert (neq A D) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists E, (BetS A C E /\ Cong C E A D)) by (conclude lemma_extension);destruct Tf as [E];spliter.
(* Goal: @eq Ax0 C D *)
assert (BetS A B E) by (conclude lemma_3_6b).
(* Goal: @eq Ax0 C D *)
assert (~ eq A D).
(* Goal: not (@eq Ax0 A D) *)
(* Goal: @eq Ax0 C D *)
 {
(* Goal: not (@eq Ax0 A D) *)
 intro.
(* Goal: False *)
 assert (BetS A B A) by (conclude cn_equalitysub).
(* Goal: False *)
 assert (~ BetS A B A) by (conclude axiom_betweennessidentity).
(* Goal: False *)
 contradict.
 }
(* Goal: @eq Ax0 C D *)
assert (neq A C) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists F, (BetS A D F /\ Cong D F A C)) by (conclude lemma_extension);destruct Tf as [F];spliter.
(* Goal: @eq Ax0 C D *)
assert (BetS F D A) by (conclude axiom_betweennesssymmetry).
(* Goal: @eq Ax0 C D *)
assert (BetS D B A) by (conclude axiom_betweennesssymmetry).
(* Goal: @eq Ax0 C D *)
assert (BetS F B A) by (conclude lemma_3_5b).
(* Goal: @eq Ax0 C D *)
assert (BetS A B F) by (conclude axiom_betweennesssymmetry).
(* Goal: @eq Ax0 C D *)
assert (Cong F D D F) by (conclude cn_equalityreverse).
(* Goal: @eq Ax0 C D *)
assert (Cong F D A C) by (conclude lemma_congruencetransitive).
(* Goal: @eq Ax0 C D *)
assert (Cong A D C E) by (conclude lemma_congruencesymmetric).
(* Goal: @eq Ax0 C D *)
assert (Cong D A A D) by (conclude cn_equalityreverse).
(* Goal: @eq Ax0 C D *)
assert (Cong D A C E) by (conclude lemma_congruencetransitive).
(* Goal: @eq Ax0 C D *)
assert (Cong F A A E) by (conclude cn_sumofparts).
(* Goal: @eq Ax0 C D *)
assert (Cong A E F A) by (conclude lemma_congruencesymmetric).
(* Goal: @eq Ax0 C D *)
assert (Cong F A A F) by (conclude cn_equalityreverse).
(* Goal: @eq Ax0 C D *)
assert (Cong A E A F) by (conclude lemma_congruencetransitive).
(* Goal: @eq Ax0 C D *)
assert (Cong A B A B) by (conclude cn_congruencereflexive).
(* Goal: @eq Ax0 C D *)
assert (Cong B E B F) by (conclude lemma_differenceofparts).
(* Goal: @eq Ax0 C D *)
assert (eq E F) by (conclude lemma_extensionunique).
(* Goal: @eq Ax0 C D *)
assert (BetS A D E) by (conclude cn_equalitysub).
(* Goal: @eq Ax0 C D *)
assert (BetS B C E) by (conclude lemma_3_6a).
(* Goal: @eq Ax0 C D *)
assert (BetS B D E) by (conclude lemma_3_6a).
(* Goal: @eq Ax0 C D *)
assert (eq C D) by (conclude axiom_connectivity).
(* Goal: @eq Ax0 C D *)
close.
Qed.

End Euclid.


