proposition: Lemma l11_60 : forall A B C D E P, ~ Col A B C -> Per A D P -> Per B D P -> Per C D P -> Coplanar A B C E -> Per E D P.
proof: Proof. intros A B C D E P HNCol HPerA HPerB HPerC HCop. destruct (eq_dec_points D P). subst; apply l8_5. destruct (symmetric_point_construction P D) as [P']. exists P'; split; auto. apply (l11_60_aux A B C); [|apply per_double_cong with D..|]; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2