proposition: Lemma cop3_orth__orth : forall A B C D E F U V, ~ Col D E F -> Coplanar A B C D -> Coplanar A B C E -> Coplanar A B C F -> Orth A B C U V -> Orth D E F U V.
proof: Proof. intros A B C D E F U V HNCol HD HE HF [X HX]. exists X. apply (cop3_orth_at__orth_at A B C); assumption. Qed.
imports: GeoCoq.Tarski_dev.Ch10_line_reflexivity_2