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