proposition: Lemma point_construction_different : forall A B, exists C, Bet A B C /\ B <> C.
proof: Proof. intros. assert (tdp := two_distinct_points). ex_elim tdp x. ex_elim H y. prolong A B F x y. exists F. show_distinct B F. intuition. intuition. Qed.
imports: GeoCoq.Tarski_dev.Ch02_cong