proposition: Lemma outer_transitivity_between2 : forall A B C D, Bet A B C -> Bet B C D -> B<>C -> Bet A C D.
proof: Proof. intros. prolong A C x C D. assert (x = D) by (apply (construction_uniqueness B C C D); try apply (between_exchange3 A B C x); Cong). subst x;assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch02_cong