proposition: Lemma perp_inter_perp_in_n : forall A B C D : Tpoint, Perp A B C D -> exists P : Tpoint, Col A B P /\ Col C D P /\ Perp_at P A B C D.
proof: Proof. intros. assert(A <> B /\ C <> D). apply perp_distinct in H. tauto. spliter. induction(col_dec A B C). exists C. split; Col. split; Col. apply(l8_14_2_1b_bis A B C D C); Col. assert(HH:=l8_18_existence A B C H2). ex_and HH P. exists P. assert(Col C D P). apply(cop_perp2__col C D P A B); Perp. exists P. left. split; Col. split; Col. split; Col. apply(l8_14_2_1b_bis A B C D P); Col. Qed.
imports: GeoCoq.Tarski_dev.Ch12_parallel