proposition: Lemma l11_62_existence_bis : forall A B C P, ~ Coplanar A B C P -> exists X, Orth_at X A B C X P.
proof: Proof. intros A B C P HNCop. destruct (l11_62_existence A B C P) as [X [HCop HX]]. assert (X <> P) by (intro; subst; apply (HNCop HCop)). exists X; repeat split; Col. apply ncop__ncol with P, HNCop. intros D Q HD HQ. apply per_col with P; auto. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2