Require Export GeoCoq.Elements.OriginalProofs.euclidean_tactics.

Section Euclid.

Context `{Ax:euclidean_neutral}.

Lemma lemma_3_6a : 
   forall A B C D, 
   BetS A B C -> BetS A C D ->
   BetS B C D.
Proof.
(* Goal: forall (A B C D : @Point Ax) (_ : @BetS Ax A B C) (_ : @BetS Ax A C D), @BetS Ax B C D *)
intros.
(* Goal: @BetS Ax B C D *)
assert (BetS C B A) by (conclude axiom_betweennesssymmetry).
(* Goal: @BetS Ax B C D *)
assert (BetS D C A) by (conclude axiom_betweennesssymmetry).
(* Goal: @BetS Ax B C D *)
assert (BetS D C B) by (conclude axiom_innertransitivity).
(* Goal: @BetS Ax B C D *)
assert (BetS B C D) by (conclude axiom_betweennesssymmetry).
(* Goal: @BetS Ax B C D *)
close.
Qed.

End Euclid.

