proposition: Lemma invert_two_sides : forall A B P Q, TS A B P Q -> TS B A P Q.
proof: Proof. Proof with Col. unfold TS. intros. spliter. repeat split... ex_and H1 T. exists T;split... Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar