proposition: Lemma l11_63_existence : forall A B C D P, Coplanar A B C D -> ~ Coplanar A B C P -> exists Q, Orth A B C D Q.
proof: Proof. intros A B C D P HCop HNCop. destruct (l11_62_existence_bis A B C P HNCop) as [E HE]. destruct (eq_dec_points D E). exists P, D; subst; assumption. destruct (l11_63_aux A B C D E P) as [Q []]; auto. exists Q; assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2