proposition: Lemma perp_inter_perp_in : forall A B C D, Perp A B C D -> exists P, Col A B P /\ Col C D P /\ Perp_at P A B C D.
proof: Proof. intros. assert(HH:=perp_inter_exists A B C D H). ex_and HH P. exists P. split. Col. split. Col. apply l8_14_2_1b_bis; Col. Qed.
imports: GeoCoq.Tarski_dev.Ch11_angles