proposition: Lemma two_distinct_points : exists X, exists Y: Tpoint, X <> Y.
proof: Proof. assert (ld:=lower_dim_ex). ex_elim ld A. ex_elim H B. ex_elim H0 C. exists A; exists B. intro; subst; apply H. right; right; apply between_trivial. Qed.
imports: GeoCoq.Tarski_dev.Ch02_cong