proposition: Lemma lemma_3_7a : forall A B C D, BetS A B C -> BetS B C D -> BetS A C D.
proof: Proof. intros. assert (neq A C) by (forward_using lemma_betweennotequal). 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. assert (Cong C D C E) by (conclude lemma_congruencesymmetric). assert (BetS B C E) by (conclude lemma_3_6a). assert (eq D E) by (conclude lemma_extensionunique). assert (BetS A C D) by (conclude cn_equalitysub). close. Qed.
imports: GeoCoq.Elements.OriginalProofs.lemma_betweennotequal GeoCoq.Elements.OriginalProofs.lemma_localextension GeoCoq.Elements.OriginalProofs.lemma_extensionunique