proposition: Lemma outer_transitivity_between : forall A B C D, Bet A B C -> Bet B C D -> B<>C -> Bet A B D.
proof: Proof. intros. apply between_symmetry. apply (outer_transitivity_between2) with C; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch02_cong