proposition: Lemma l9_38 : forall A B C P Q, TSP A B C P Q -> TSP A B C Q P.
proof: Proof. intros A B C P Q [HP [HQ [T [HT HBet]]]]. repeat split; trivial. exists T; split; Between. Qed.
imports: GeoCoq.Tarski_dev.Ch08_orthogonality GeoCoq.Tarski_dev.Annexes.coplanar