Require Export GeoCoq.Elements.OriginalProofs.lemma_betweennotequal.
Require Export GeoCoq.Elements.OriginalProofs.lemma_localextension.
Require Export GeoCoq.Elements.OriginalProofs.lemma_extensionunique.

Section Euclid.
Context `{Ax:euclidean_neutral_ruler_compass}.
Lemma lemma_3_7a : 
   forall A B C D, 
   BetS A B C -> BetS B C D ->
   BetS A C D.
Proof.
(* Goal: forall (A B C D : @Point Ax0) (_ : @BetS Ax0 A B C) (_ : @BetS Ax0 B C D), @BetS Ax0 A C D *)
intros.
(* Goal: @BetS Ax0 A C D *)
assert (neq A C) by (forward_using lemma_betweennotequal).
(* Goal: @BetS Ax0 A C D *)
assert (neq C D) by (forward_using lemma_betweennotequal).
let Tf:=fresh in
assert (Tf:exists E, (BetS A C E /\ Cong C E C D)) by (conclude lemma_localextension);destruct Tf as [E];spliter.
(* Goal: @BetS Ax0 A C D *)
assert (Cong C D C E) by (conclude lemma_congruencesymmetric).
(* Goal: @BetS Ax0 A C D *)
assert (BetS B C E) by (conclude lemma_3_6a).
(* Goal: @BetS Ax0 A C D *)
assert (eq D E) by (conclude lemma_extensionunique).
(* Goal: @BetS Ax0 A C D *)
assert (BetS A C D) by (conclude cn_equalitysub).
(* Goal: @BetS Ax0 A C D *)
close.
Qed.

End Euclid.

