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