proposition: Lemma distinct : forall P Q R : Tpoint, P <> Q -> (R <> P \/ R <> Q).
proof: Proof. intros. induction (eq_dec_points R P). subst R. right. assumption. left. assumption. Qed.
imports: GeoCoq.Tarski_dev.Definitions GeoCoq.Tactics.finish