Require Export GeoCoq.Elements.OriginalProofs.lemma_3_7a.

Section Euclid.

Context `{Ax:euclidean_neutral_ruler_compass}.

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

End Euclid.


