proposition: Lemma between_trivial : forall A B : Tpoint, Bet A B B.
proof: Proof. intros. prolong A B x B B. assert (x = B) by (apply cong_reverse_identity with B; Cong). subst;assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch02_cong