proposition: Lemma ts_distincts : forall A B P Q, TS A B P Q -> A <> B /\ A <> P /\ A <> Q /\ B <> P /\ B <> Q /\ P <> Q.
proof: Proof. intros A B P Q HTS. destruct HTS as [HNCol1 [HNCol2 [T [HCol HBet]]]]. assert_diffs. repeat split; auto. intro; treat_equalities; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar