proposition: Lemma between_exchange3 : forall A B C D, Bet A B C -> Bet A C D -> Bet B C D.
proof: Proof. intros. assert (exists x, Bet C x C /\ Bet B x D) by (apply inner_pasch with A; apply between_symmetry; auto). ex_and H1 x. assert (C = x) by (apply between_identity; auto); subst; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch02_cong