proposition: Lemma not_two_sides_id : forall A P Q, ~ TS P Q A A.
proof: Proof. intros. intro. unfold TS in H. spliter. ex_and H1 T. apply between_identity in H2. subst T. apply H0. apply H1. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar