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