proposition: Lemma perp_inter_exists : forall A B C D, Perp A B C D -> exists P, Col A B P /\ Col C D P.
proof: Proof. intros A B C D HPerp. destruct HPerp as [P [_ [_ [HCol1 [HCol2]]]]]. exists P; split; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles