proposition: Lemma l11_60_bis : forall A B C D P, ~ Col A B C -> D <> P -> Coplanar A B C D -> Per A D P -> Per B D P -> Per C D P -> Orth_at D A B C D P.
proof: Proof. intros A B C D P HNCol HDP HD HA HB HC. repeat split; Col. intros E Q HE HQ. apply per_col with P; auto. apply (l11_60 A B C); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2