proposition: Lemma tsp_distincts : forall A B C P Q, TSP A B C P Q -> A <> B /\ A <> C /\ B <> C /\ A <> P /\ B <> P /\ C <> P /\ A <> Q /\ B <> Q /\ C <> Q /\ P <> Q.
proof: Proof. intros A B C P Q [HP [HQ HT]]. assert (HP' := ncop_distincts A B C P HP). assert (HQ' := ncop_distincts A B C Q HQ). spliter; clean. repeat split; auto. destruct HT; spliter. intro; apply HP; treat_equalities; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar